[GHC] #16008: GHC HEAD type family regression involving invisible arguments

[GHC]

#16008: GHC HEAD type family regression involving invisible arguments
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.8.1
       Component:  Compiler (Type    |              Version:  8.7
  checker)                           |             Keywords:  TypeFamilies,
      Resolution:                    |  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 The following patch makes the original program compile again:

 {{{#!diff
 diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs
 index 284d6a95d3..991f7eb859 100644
 --- a/compiler/typecheck/Inst.hs
 +++ b/compiler/typecheck/Inst.hs
 @@ -487,18 +487,19 @@ no longer cut it, but it seems fine for now.
  -- | Instantantiate the TyConBinders of a forall type,
  --   given its decomposed form (tvs, ty)
  tcInstTyBinders :: HasDebugCallStack
 -              => ([TyCoBinder], TcKind)   -- ^ The type (forall bs. ty)
 +              => Maybe (VarEnv Kind)
 +              -> ([TyCoBinder], TcKind)   -- ^ The type (forall bs. ty)
                -> TcM ([TcType], TcKind)   -- ^ Instantiated bs,
 substituted ty
  -- Takes a pair because that is what splitPiTysInvisible returns
  -- See also Note [Bidirectional type checking]
 -tcInstTyBinders (bndrs, ty)
 +tcInstTyBinders mb_kind_info (bndrs, ty)
    | null bndrs        -- It's fine for bndrs to be empty e.g.
    = return ([], ty)   -- Check that (Maybe :: forall {k}. k->*),
                        --       and see the call to instTyBinders in
 checkExpectedKind
                        -- A user bug to be reported as such; it is not a
 compiler crash!

    | otherwise
 -  = do { (subst, args) <- mapAccumLM (tcInstTyBinder Nothing) empty_subst
 bndrs
 +  = do { (subst, args) <- mapAccumLM (tcInstTyBinder mb_kind_info)
 empty_subst bndrs
         ; ty' <- zonkTcType (substTy subst ty)
                     -- Why zonk the result? So that tcTyVar can
                     -- obey (IT6) of Note [The tcType invariant] in
 TcHsType
 diff --git a/compiler/typecheck/TcHsType.hs
 b/compiler/typecheck/TcHsType.hs
 index 3b36281d4a..39f26949ae 100644
 --- a/compiler/typecheck/TcHsType.hs
 +++ b/compiler/typecheck/TcHsType.hs
 @@ -1021,7 +1021,7 @@ checkExpectedKindX pp_hs_ty ty act_kind exp_kind
          let n_exp_invis_bndrs = invisibleTyBndrCount exp_kind
              n_act_invis_bndrs = invisibleTyBndrCount act_kind
              n_to_inst         = n_act_invis_bndrs - n_exp_invis_bndrs
 -      ; (new_args, act_kind') <- tcInstTyBinders (splitPiTysInvisibleN
 n_to_inst act_kind)
 +      ; (new_args, act_kind') <- tcInstTyBinders Nothing
 (splitPiTysInvisibleN n_to_inst act_kind)

        ; let origin = TypeEqOrigin { uo_actual   = act_kind'
                                    , uo_expected = exp_kind
 @@ -1133,7 +1133,7 @@ tcTyVar mode name         -- Could be a tyvar, a
 tycon, or a datacon
        | otherwise
        = do { let tc_arity = tyConArity tc
             ; tc_kind <- zonkTcType (tyConKind tc)
 -           ; (tc_args, kind) <- tcInstTyBinders (splitPiTysInvisibleN
 tc_arity tc_kind)
 +           ; (tc_args, kind) <- tcInstTyBinders Nothing
 (splitPiTysInvisibleN tc_arity tc_kind)
                   -- Instantiate enough invisible arguments
                   -- to saturate the family TyCon

 diff --git a/compiler/typecheck/TcTyClsDecls.hs
 b/compiler/typecheck/TcTyClsDecls.hs
 index 877166dfd5..0700f94202 100644
 --- a/compiler/typecheck/TcTyClsDecls.hs
 +++ b/compiler/typecheck/TcTyClsDecls.hs
 @@ -1895,13 +1895,17 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars
 exp_bndrs hs_pats hs_rhs_ty
         ; return (qtvs, pats, rhs_ty) }
    where
      tc_lhs | null hs_pats  -- See Note [Apparently-nullary families]
 -           = do { (args, rhs_kind) <- tcInstTyBinders $
 +           = do { (args, rhs_kind) <- tcInstTyBinders mb_kind_env $
                                        splitPiTysInvisibleN (tyConArity
 fam_tc)
                                                             (tyConKind
 fam_tc)
                  ; return (mkTyConApp fam_tc args, rhs_kind) }
             | otherwise
             = tcFamTyPats fam_tc mb_clsinfo hs_pats

 +    mb_kind_env = case mb_clsinfo of
 +                    NotAssociated -> Nothing
 +                    InClsInst{ai_inst_env = kind_env} -> Just kind_env
 +
  {- Note [Apparently-nullary families]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  Consider
 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/testsuite/tests/indexed-types/should_fail/T9160.stderr
 +++ b/testsuite/tests/indexed-types/should_fail/T9160.stderr
 @@ -1,7 +1,7 @@

 -T9160.hs:19:3: error:
 -    • Type indexes must match class instance head
 -      Expected: F @*
 -        Actual: F @(* -> *)
 -    • In the type instance declaration for ‘F’
 +T9160.hs:19:12: error:
 +    • Expecting one more argument to ‘Maybe’
 +      Expected a type, but ‘Maybe’ has kind ‘* -> *’
 +    • In the type ‘Maybe’
 +      In the type instance declaration for ‘F’
        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.)

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16008#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler