Document and simplify tcInstTyBinders

This fixes #15282.

compiler/typecheck/Inst.hs

@@ -15,7 +15,7 @@ module Inst (
        instCall, instDFunType, instStupidTheta, instTyVarsWith,
        newWanted, newWanteds,
 
-       tcInstBinders, tcInstBinder,
+       tcInstTyBinders, tcInstTyBinder,
 
        newOverloadedLit, mkOverLit,
 
@@ -410,25 +410,97 @@ instStupidTheta orig theta
 *                                                                      *
 ************************************************************************
 
+Note [Constraints handled in types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Generally, we cannot handle constraints written in types. For example,
+if we declare
+
+  data C a where
+    MkC :: Show a => a -> C a
+
+we will not be able to use MkC in types, as we have no way of creating
+a type-level Show dictionary.
+
+However, we make an exception for equality types. Consider
+
+  data T1 a where
+    MkT1 :: T1 Bool
+
+  data T2 a where
+    MkT2 :: a ~ Bool => T2 a
+
+MkT1 has a constrained return type, while MkT2 uses an explicit equality
+constraint. These two types are often written interchangeably, with a
+reasonable expectation that they mean the same thing. For this to work --
+and for us to be able to promote GADTs -- we need to be able to instantiate
+equality constraints in types.
+
+One wrinkle is that the equality in MkT2 is *lifted*. But, for proper
+GADT equalities, GHC produces *unlifted* constraints. (This unlifting comes
+from DataCon.eqSpecPreds, which uses mkPrimEqPred.) And, perhaps a wily
+user will use (~~) for a heterogeneous equality. We thus must support
+all of (~), (~~), and (~#) in types. (See Note [The equality types story]
+in TysPrim for a primer on these equality types.)
+
+The get_eq_tys_maybe function recognizes these three forms of equality,
+returning a suitable type formation function and the two types related
+by the equality constraint. In the lifted case, it uses mkHEqBoxTy or
+mkEqBoxTy, which promote the datacons of the (~~) or (~) datatype,
+respectively.
+
+One might reasonably wonder who *unpacks* these boxes once they are
+made. After all, there is no type-level `case` construct. The surprising
+answer is that no one ever does. Instead, if a GADT constructor is used
+on the left-hand side of a type family equation, that occurrence forces
+GHC to unify the types in question. For example:
+
+  data G a where
+    MkG :: G Bool
+
+  type family F (x :: G a) :: a where
+    F MkG = False
+
+When checking the LHS `F MkG`, GHC sees the MkG constructor and then must
+unify F's implicit parameter `a` with Bool. This succeeds, making the equation
+
+    F Bool (MkG @Bool <Bool>) = False
+
+Note that we never need unpack the coercion. This is because type family
+equations are *not* parametric in their kind variables. That is, we could have
+just said
+
+  type family H (x :: G a) :: a where
+    H _ = False
+
+The presence of False on the RHS also forces `a` to become Bool, giving us
+
+    H Bool _ = False
+
+The fact that any of this works stems from the lack of phase separation between
+types and kinds (unlike the very present phase separation between terms and types).
+
+Once we have the ability to pattern-match on types below top-level, this will
+no longer cut it, but it seems fine for now.
+
 -}
 
 ---------------------------
 -- | This is used to instantiate binders when type-checking *types* only.
 -- The @VarEnv Kind@ gives some known instantiations.
 -- See also Note [Bidirectional type checking]
-tcInstBinders :: TCvSubst -> Maybe (VarEnv Kind)
-               -> [TyBinder] -> TcM (TCvSubst, [TcType])
-tcInstBinders subst mb_kind_info bndrs
-  = do { (subst, args) <- mapAccumLM (tcInstBinder mb_kind_info) subst bndrs
+tcInstTyBinders :: TCvSubst -> Maybe (VarEnv Kind)
+                -> [TyBinder] -> TcM (TCvSubst, [TcType])
+tcInstTyBinders subst mb_kind_info bndrs
+  = do { (subst, args) <- mapAccumLM (tcInstTyBinder mb_kind_info) subst bndrs
        ; traceTc "instantiating tybinders:"
            (vcat $ zipWith (\bndr arg -> ppr bndr <+> text ":=" <+> ppr arg)
                            bndrs args)
        ; return (subst, args) }
 
 -- | Used only in *types*
-tcInstBinder :: Maybe (VarEnv Kind)
-              -> TCvSubst -> TyBinder -> TcM (TCvSubst, TcType)
-tcInstBinder mb_kind_info subst (Named (TvBndr tv _))
+tcInstTyBinder :: Maybe (VarEnv Kind)
+               -> TCvSubst -> TyBinder -> TcM (TCvSubst, TcType)
+tcInstTyBinder mb_kind_info subst (Named (TvBndr tv _))
   = case lookup_tv tv of
       Just ki -> return (extendTvSubstAndInScope subst tv ki, ki)
       Nothing -> do { (subst', tv') <- newMetaTyVarX subst tv
@@ -438,18 +510,11 @@ tcInstBinder mb_kind_info subst (Named (TvBndr tv _))
                       ; lookupVarEnv env tv }
 
 
-tcInstBinder _ subst (Anon ty)
+tcInstTyBinder _ subst (Anon ty)
      -- This is the *only* constraint currently handled in types.
-  | Just (mk, role, k1, k2) <- get_pred_tys_maybe substed_ty
-  = do { let origin = TypeEqOrigin { uo_actual   = k1
-                                   , uo_expected = k2
-                                   , uo_thing    = Nothing
-                                   , uo_visible  = True }
-       ; co <- case role of
-                 Nominal          -> unifyKind Nothing k1 k2
-                 Representational -> emitWantedEq origin KindLevel role k1 k2
-                 Phantom          -> pprPanic "tcInstBinder Phantom" (ppr ty)
-       ; arg' <- mk co k1 k2
+  | Just (mk, k1, k2) <- get_eq_tys_maybe substed_ty
+  = do { co <- unifyKind Nothing k1 k2
+       ; arg' <- mk co
        ; return (subst, arg') }
 
   | isPredTy substed_ty
@@ -469,20 +534,33 @@ tcInstBinder _ subst (Anon ty)
   where
     substed_ty = substTy subst ty
 
-      -- handle boxed equality constraints, because it's so easy
-    get_pred_tys_maybe ty
-      | Just (r, k1, k2) <- getEqPredTys_maybe ty
-      = Just (\co _ _ -> return $ mkCoercionTy co, r, k1, k2)
+      -- See Note [Constraints handled in types]
+    get_eq_tys_maybe :: Type
+                     -> Maybe ( Coercion -> TcM Type
+                                 -- given a coercion proving t1 ~# t2, produce the
+                                 -- right instantiation for the TyBinder at hand
+                              , Type  -- t1
+                              , Type  -- t2
+                              )
+    get_eq_tys_maybe ty
+        -- unlifted equality (~#)
+      | Just (Nominal, k1, k2) <- getEqPredTys_maybe ty
+      = Just (\co -> return $ mkCoercionTy co, k1, k2)
+
+        -- lifted heterogeneous equality (~~)
       | Just (tc, [_, _, k1, k2]) <- splitTyConApp_maybe ty
       = if | tc `hasKey` heqTyConKey
-             -> Just (mkHEqBoxTy, Nominal, k1, k2)
+             -> Just (\co -> mkHEqBoxTy co k1 k2, k1, k2)
            | otherwise
              -> Nothing
+
+        -- lifted homogeneous equality (~)
       | Just (tc, [_, k1, k2]) <- splitTyConApp_maybe ty
       = if | tc `hasKey` eqTyConKey
-             -> Just (mkEqBoxTy, Nominal, k1, k2)
+             -> Just (\co -> mkEqBoxTy co k1 k2, k1, k2)
            | otherwise
              -> Nothing
+
       | otherwise
       = Nothing
 

compiler/typecheck/TcHsType.hs

@@ -70,7 +70,7 @@ import TcIface
 import TcSimplify
 import TcType
 import TcHsSyn( zonkSigType )
-import Inst   ( tcInstBinders, tcInstBinder )
+import Inst   ( tcInstTyBinders, tcInstTyBinder )
 import TyCoRep( TyBinder(..) )  -- Used in tcDataKindSig
 import Type
 import Coercion
@@ -508,7 +508,7 @@ metavariable.
 In types, however, we're not so lucky, because *we cannot re-generalize*!
 There is no lambda. So, we must be careful only to instantiate at the last
 possible moment, when we're sure we're never going to want the lost polymorphism
-again. This is done in calls to tcInstBinders.
+again. This is done in calls to tcInstTyBinders.
 
 To implement this behavior, we use bidirectional type checking, where we
 explicitly think about whether we know the kind of the type we're checking
@@ -951,7 +951,7 @@ tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
       | isInvisibleBinder ki_binder
         -- It's invisible. Instantiate.
       = do { traceTc "tcInferApps (invis)" (ppr ki_binder $$ ppr subst)
-           ; (subst', arg') <- tcInstBinder mb_kind_info subst ki_binder
+           ; (subst', arg') <- tcInstTyBinder mb_kind_info subst ki_binder
            ; go n (arg' : acc_args) subst' (mkNakedAppTy fun arg')
                 ki_binders inner_ki all_args }
 
@@ -1072,7 +1072,7 @@ instantiateTyN mb_kind_env n bndrs inner_ki
   = return ([], ki)
 
   | otherwise
-  = do { (subst, inst_args) <- tcInstBinders empty_subst mb_kind_env inst_bndrs
+  = do { (subst, inst_args) <- tcInstTyBinders empty_subst mb_kind_env inst_bndrs
        ; let rebuilt_ki = mkPiTys leftover_bndrs inner_ki
              ki'        = substTy subst rebuilt_ki
        ; traceTc "instantiateTyN" (vcat [ ppr ki

compiler/typecheck/TcMType.hs

@@ -911,7 +911,7 @@ new_meta_tv_x info subst tv
       -- is not yet fixed so leaving as unchecked for now.
       -- OLD NOTE:
       -- Unchecked because we call newMetaTyVarX from
-      -- tcInstBinder, which is called from tc_infer_args
+      -- tcInstTyBinder, which is called from tcInferApps
       -- which does not yet take enough trouble to ensure
       -- the in-scope set is right; e.g. Trac #12785 trips
       -- if we use substTy here