Opened 9 months ago

Closed 9 months ago

#16008 closed bug (fixed)

GHC HEAD type family regression involving invisible arguments

Reported by: RyanGlScott Owned by:
Priority: highest Milestone: 8.8.1
Component: Compiler (Type checker) Version: 8.7
Keywords: TypeFamilies, TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: typecheck/should_compile/T16008
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D5435
Wiki Page:

Description

The following code compiles on GHC 8.0.2 through 8.6.2:

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind

class C k where
  type S :: k -> Type

data D :: Type -> Type
data SD :: forall a. D a -> Type

instance C (D a) where
  type S = SD

But fails to compile on GHC HEAD (commit 73cce63f33ee80f5095085141df9313ac70d1cfa):

$ ~/Software/ghc2/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:15:3: error:
    • Type indexes must match class instance head
      Expected: S @(D a)
        Actual: S @(D a1)
    • In the type instance declaration for ‘S’
      In the instance declaration for ‘C (D a)’
   |
15 |   type S = SD
   |   ^^^^^^^^^^^

This regression prevents the stitch library from compiling.

Change History (7)

comment:1 Changed 9 months ago by RyanGlScott

A workaround is to manually give SD a kind ascription:

instance C (D a) where
  type S = (SD :: D a -> Type)

comment:2 Changed 9 months ago by RyanGlScott

I haven't confirmed this yet, but I believe the culprit is this part of tcTyFamInstEqnGuts:

    tc_lhs | null hs_pats  -- See Note [Apparently-nullary families]
           = do { (args, rhs_kind) <- tcInstTyBinders $
                                      splitPiTysInvisibleN (tyConArity fam_tc)
                                                           (tyConKind  fam_tc)
                ; return (mkTyConApp fam_tc args, rhs_kind) }
           | otherwise
           = tcFamTyPats fam_tc mb_clsinfo hs_pats

In the null hs_pats case, we are calling tcInstTyBinders, but that doesn't take the class-bound variables (in mb_clsinfo) into account! Some evidence which supports this theory:

  1. The otherwise case (when the type family takes at least one argument) does take mb_clsinfo into account. You can see for yourself that this code works correctly by observing that this variant of the original program typechecks:
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind

class C k where
  type S z :: k -> Type

data D :: Type -> Type
data SD :: forall a. D a -> Type

instance C (D a) where
  type S z = SD
  1. Before commit 2257a86daa72db382eb927df12a718669d5491f8 (Taming the Kind Inference Monster), which introduced this regression, the code that corresponded to tc_lhs was this:
kcTyFamEqnRhs mb_clsinfo rhs_hs_ty lhs_ki
  = do { -- It's still possible the lhs_ki has some foralls. Instantiate these away.
         (new_pats, insted_lhs_ki)
           <- instantiateTyUntilN mb_kind_env 0 lhs_ki

This code uses a function which is aware of the class-bound variables (mb_kind_env).

comment:3 Changed 9 months ago by RyanGlScott

The following patch makes the original program compile again:

  • compiler/typecheck/Inst.hs

    diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs
    index 284d6a95d3..991f7eb859 100644
    a b no longer cut it, but it seems fine for now. 
    487487-- | Instantantiate the TyConBinders of a forall type,
    488488--   given its decomposed form (tvs, ty)
    489489tcInstTyBinders :: HasDebugCallStack
    490               => ([TyCoBinder], TcKind)   -- ^ The type (forall bs. ty)
     490              => Maybe (VarEnv Kind)
     491              -> ([TyCoBinder], TcKind)   -- ^ The type (forall bs. ty)
    491492              -> TcM ([TcType], TcKind)   -- ^ Instantiated bs, substituted ty
    492493-- Takes a pair because that is what splitPiTysInvisible returns
    493494-- See also Note [Bidirectional type checking]
    494 tcInstTyBinders (bndrs, ty)
     495tcInstTyBinders mb_kind_info (bndrs, ty)
    495496  | null bndrs        -- It's fine for bndrs to be empty e.g.
    496497  = return ([], ty)   -- Check that (Maybe :: forall {k}. k->*),
    497498                      --       and see the call to instTyBinders in checkExpectedKind
    498499                      -- A user bug to be reported as such; it is not a compiler crash!
    499500
    500501  | otherwise
    501   = do { (subst, args) <- mapAccumLM (tcInstTyBinder Nothing) empty_subst bndrs
     502  = do { (subst, args) <- mapAccumLM (tcInstTyBinder mb_kind_info) empty_subst bndrs
    502503       ; ty' <- zonkTcType (substTy subst ty)
    503504                   -- Why zonk the result? So that tcTyVar can
    504505                   -- obey (IT6) of Note [The tcType invariant] in TcHsType
  • compiler/typecheck/TcHsType.hs

    diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
    index 3b36281d4a..39f26949ae 100644
    a b checkExpectedKindX pp_hs_ty ty act_kind exp_kind 
    10211021        let n_exp_invis_bndrs = invisibleTyBndrCount exp_kind
    10221022            n_act_invis_bndrs = invisibleTyBndrCount act_kind
    10231023            n_to_inst         = n_act_invis_bndrs - n_exp_invis_bndrs
    1024       ; (new_args, act_kind') <- tcInstTyBinders (splitPiTysInvisibleN n_to_inst act_kind)
     1024      ; (new_args, act_kind') <- tcInstTyBinders Nothing (splitPiTysInvisibleN n_to_inst act_kind)
    10251025
    10261026      ; let origin = TypeEqOrigin { uo_actual   = act_kind'
    10271027                                  , uo_expected = exp_kind
    tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon 
    11331133      | otherwise
    11341134      = do { let tc_arity = tyConArity tc
    11351135           ; tc_kind <- zonkTcType (tyConKind tc)
    1136            ; (tc_args, kind) <- tcInstTyBinders (splitPiTysInvisibleN tc_arity tc_kind)
     1136           ; (tc_args, kind) <- tcInstTyBinders Nothing (splitPiTysInvisibleN tc_arity tc_kind)
    11371137                 -- Instantiate enough invisible arguments
    11381138                 -- to saturate the family TyCon
    11391139
  • compiler/typecheck/TcTyClsDecls.hs

    diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
    index 877166dfd5..0700f94202 100644
    a b tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty 
    18951895       ; return (qtvs, pats, rhs_ty) }
    18961896  where
    18971897    tc_lhs | null hs_pats  -- See Note [Apparently-nullary families]
    1898            = do { (args, rhs_kind) <- tcInstTyBinders $
     1898           = do { (args, rhs_kind) <- tcInstTyBinders mb_kind_env $
    18991899                                      splitPiTysInvisibleN (tyConArity fam_tc)
    19001900                                                           (tyConKind  fam_tc)
    19011901                ; return (mkTyConApp fam_tc args, rhs_kind) }
    19021902           | otherwise
    19031903           = tcFamTyPats fam_tc mb_clsinfo hs_pats
    19041904
     1905    mb_kind_env = case mb_clsinfo of
     1906                    NotAssociated -> Nothing
     1907                    InClsInst{ai_inst_env = kind_env} -> Just kind_env
     1908
    19051909{- Note [Apparently-nullary families]
    19061910~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    19071911Consider
  • testsuite/tests/indexed-types/should_fail/T9160.stderr

    diff --git a/testsuite/tests/indexed-types/should_fail/T9160.stderr b/testsuite/tests/indexed-types/should_fail/T9160.stderr
    index e918013f67..14f204191e 100644
    a b  
    11
    2 T9160.hs:19:3: error:
    3     • Type indexes must match class instance head
    4       Expected: F @*
    5         Actual: F @(* -> *)
    6     In the type instance declaration for ‘F’
     2T9160.hs:19:12: error:
     3    • Expecting one more argument to ‘Maybe’
     4      Expected a type, but ‘Maybe’ has kind ‘* -> *’
     5    • In the type ‘Maybe’
     6      In the type instance declaration for ‘F’
    77      In the instance declaration for ‘C (a :: *)’

As you can see, there is one existing test (T9160) whose expected stderr changed, but the new error message arguably makes as much sense as the previous one. (For what it's worth, that new error message used to be the expected stderr before commit https://ghc.haskell.org/trac/ghc/changeset/2257a86daa72db382eb927df12a718669d5491f8/ghc landed.)

comment:4 Changed 9 months ago by goldfire

I know Simon strongly disliked that Maybe (VarEnv Kind) getting too far from TcTyClsDecls.

Could you just add a call to addConsistencyConstraints to tc_lhs? I also think that the new checkExpectedKind from Phab:D5229 will fix this handily.

comment:5 Changed 9 months ago by RyanGlScott

Differential Rev(s): Phab:D5435
Status: newpatch

Oh wow, I was not aware of checkConsistencyConstraints! That's a much cleaner solution, and better yet, it doesn't cause any existing tests to change their expected output.

I've submitted a patch as Phab:D5435.

comment:6 Changed 9 months ago by Ryan Scott <ryan.gl.scott@…>

In 3899966e/ghc:

Fix #16008 with a pinch of addConsistencyConstraints

Summary:
#16008 happened because we forgot to typecheck nullary
associated type family instances in a way that's consistent with the
type variables bound by the parent class. Oops. Easily fixed with a
use of `checkConsistencyConstraints`.

Test Plan: make test TEST=T16008

Reviewers: simonpj, goldfire, bgamari

Reviewed By: goldfire

Subscribers: rwbarton, carter

GHC Trac Issues: #16008

Differential Revision: https://phabricator.haskell.org/D5435

comment:7 Changed 9 months ago by RyanGlScott

Resolution: fixed
Status: patchclosed
Test Case: typecheck/should_compile/T16008
Note: See TracTickets for help on using tickets.