[Git][ghc/ghc][wip/int-index/decl-invis-binders] Wibble comments

[Simon Peyton Jones (@simonpj)]

Simon Peyton Jones pushed to branch wip/int-index/decl-invis-binders at Glasgow Haskell Compiler / GHC


Commits:
ee0cc50d by Simon Peyton Jones at 2023-02-03T12:46:02+00:00
Wibble comments

- - - - -


2 changed files:

- compiler/GHC/Hs/Type.hs
- compiler/GHC/Tc/TyCl.hs


Changes:

=====================================
compiler/GHC/Hs/Type.hs
=====================================
@@ -286,6 +286,8 @@ type instance XXTyVarBndr   (GhcPass _) = DataConCantHappen
 hsTyVarBndrFlag :: HsTyVarBndr flag (GhcPass pass) -> flag
 hsTyVarBndrFlag (UserTyVar _ fl _)     = fl
 hsTyVarBndrFlag (KindedTyVar _ fl _ _) = fl
+-- By specialising to (GhcPass p) we know that XXTyVarBndr is DataConCantHappen
+-- so these two equations are exhaustive: extension construction can't happen
 
 -- | Set the attached flag
 setHsTyVarBndrFlag :: flag -> HsTyVarBndr flag' (GhcPass pass)


=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -412,16 +412,22 @@ come upon knowledge of the eventual tycon in bits and pieces, and we
 use a TcTyCon to record what we know before we are ready to build the
 final TyCon.  Here is the plan:
 
-* Step 1 (inferInitialKinds, inference only, skipped for checking):
+* Step 1 (inferInitialKinds, called from kcTyClGroup
+          inference only, skipped for checking):
   Make a MonoTcTyCon whose binders are TcTyVars,
   that may contain free unification variables.
   See Note [No polymorphic recursion in type decls]
 
-* Step 2 (generaliseTcTyCon)
+* Step 2 (kcTyClDecl, called from kcTyClGroup)
+  Kind-check the declarations of the group; this step just does
+  unifications that affect the unification variables created in
+  Step 1
+
+* Step 3 (generaliseTcTyCon, called from kcTyClGroup)
   Generalise that MonoTcTyCon to make a PolyTcTyCon
   Its binders are skolem TcTyVars, with accurate SkolemInfo
 
-* Step 3 (tcTyClDecl)
+* Step 4 (tcTyClDecl, called from tcTyClDecls)
   Typecheck the type and class decls to produce a final TyCon
   Its binders are final TyVars, not TcTyVars
 
@@ -504,7 +510,7 @@ Note [No polymorphic recursion in type decls]
 In GHC.Tc.HsType.kcInferDeclHeader we use mkAnonTyConBinders to make
 the TyConBinders for the MonoTcTyCon.  Here is why.
 
-Should this kind-check?
+Should this kind-check (cf #16344)?
   data T ka (a::ka) b  = MkT (T Type           Int   Bool)
                              (T (Type -> Type) Maybe Bool)
 
@@ -536,26 +542,29 @@ all arguments when figuring out tc_binders.
 
 But notice that (#16344 comment:3)
 
-* The algorithm successfully kind-checks this declaration:
+* Consider this declaration:
     data T2 ka (a::ka) = MkT2 (T2 Type a)
 
-  Starting with inferInitialKinds:
+  Starting with inferInitialKinds
+  (Step 1 of Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon]):
     MonoTcTyCon binders:
       ka[tyv] :: (kappa1[tau] :: Type)
        a[tyv] :: (ka[tyv]     :: Type)
     MonoTcTyCon kind:
       T2 :: kappa1[tau] -> ka[tyv] -> Type
-    From (ka :: kappa1) and (ka :: Type) we learned that
-      kappa1 := Type
 
-  These constraints are soluble so generaliseTcTyCon gives
+  Given this kind for T2, in Step 2 we kind-check (T2 Type a)
+  from where we see
+    T2's first arg:  (kappa1 ~ Type)
+    T2's second arg: (ka ~ ka)
+  These constraints are soluble by (kappa1 := Type)
+  so generaliseTcTyCon (Step 3) gives
     T2 :: forall (k::Type) -> k -> *
 
-  But now the /typechecking/ (aka desugaring, tcTyClDecl) phase
-  fails, because the call (T2 Type a) in the RHS is ill-kinded.
+  But now the /typechecking/ (Step 4, aka desugaring, tcTyClDecl)
+  phase fails, because the call (T2 Type a) in the RHS is ill-kinded.
 
-  We'd really prefer all errors to show up in the kind checking
-  phase.
+  We'd really prefer all errors to show up in the kind checking phase.
 
 * This algorithm still accepts (in all phases)
      data T3 ka (a::ka) = forall b. MkT3 (T3 Type b)



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ee0cc50d6ae34ed1a7bae640cf04a218ab9b0c68

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ee0cc50d6ae34ed1a7bae640cf04a218ab9b0c68
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230203/ad50db30/attachment-0001.html>