Clean up coreView/tcView.
authorBen Gamari <ben@smart-cactus.org>
Mon, 27 Mar 2017 17:17:00 +0000 (13:17 -0400)
committerBen Gamari <ben@smart-cactus.org>
Fri, 31 Mar 2017 21:37:04 +0000 (17:37 -0400)
In Core, Constraint should be considered fully equal to
TYPE LiftedRep, in all ways. Accordingly, coreView should
unwrap Constraint to become TYPE LiftedRep. Of course, this
would be a disaster in the type checker.

So, where previously we used coreView in both the type checker
and in Core, we now have coreView and tcView, which differ only
in their treatment of Constraint.

Historical note: once upon a past, we had tcView distinct from
coreView. Back then, it was because newtypes were unwrapped in
Core but not in the type checker. The distinction is back, but
for a different reason than before.

This had a few knock-on effects:

 * The Typeable solver must explicitly handle Constraint to ensure
   that we produce the correct evidence.

 * TypeMap now respects the Constraint/Type distinction

Finished by: bgamari

Test Plan: ./validate

Reviewers: simonpj, austin, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, thomie

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

25 files changed:
compiler/coreSyn/TrieMap.hs
compiler/simplStg/RepType.hs
compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcErrors.hs
compiler/typecheck/TcForeign.hs
compiler/typecheck/TcGenFunctor.hs
compiler/typecheck/TcHsType.hs
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcTypeable.hs
compiler/typecheck/TcUnify.hs
compiler/typecheck/TcValidity.hs
compiler/types/Kind.hs
compiler/types/Type.hs
compiler/types/Type.hs-boot
compiler/types/Unify.hs
testsuite/tests/roles/should_compile/Roles14.stderr
testsuite/tests/roles/should_compile/Roles3.stderr
testsuite/tests/roles/should_compile/Roles4.stderr
testsuite/tests/roles/should_compile/T8958.stderr
testsuite/tests/typecheck/should_run/T11715.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_run/T11715.stderr [new file with mode: 0644]
testsuite/tests/typecheck/should_run/TypeOf.stdout
testsuite/tests/typecheck/should_run/TypeRep.stdout
testsuite/tests/typecheck/should_run/all.T

index f1c931d..308a953 100644 (file)
@@ -786,7 +786,9 @@ xtC (D env co) f (CoercionMapX m)
 -- but it is strictly internal to this module.  If you are including a 'TypeMap'
 -- inside another 'TrieMap', this is the type you want. Note that this
 -- lookup does not do a kind-check. Thus, all keys in this map must have
--- the same kind.
+-- the same kind. Also note that this map respects the distinction between
+-- @Type@ and @Constraint@, despite the fact that they are equivalent type
+-- synonyms in Core.
 type TypeMapG = GenMap TypeMapX
 
 -- | @TypeMapX a@ is the base map from @DeBruijn Type@ to @a@, but without the
@@ -801,13 +803,20 @@ data TypeMapX a
        }
     -- Note that there is no tyconapp case; see Note [Equality on AppTys] in Type
 
--- | squeeze out any synonyms, convert Constraint to *, and change TyConApps
--- to nested AppTys. Why the last one? See Note [Equality on AppTys] in Type
+-- | Squeeze out any synonyms, and change TyConApps to nested AppTys. Why the
+-- last one? See Note [Equality on AppTys] in Type
+--
+-- Note, however, that we keep Constraint and Type apart here, despite the fact
+-- that they are both synonyms of TYPE 'LiftedRep (see #11715).
 trieMapView :: Type -> Maybe Type
-trieMapView ty | Just ty' <- coreViewOneStarKind ty = Just ty'
 trieMapView ty
-  | Just (tc, tys@(_:_)) <- splitTyConApp_maybe ty
+  -- First check for TyConApps that need to be expanded to
+  -- AppTy chains.
+  | Just (tc, tys@(_:_)) <- tcSplitTyConApp_maybe ty
   = Just $ foldl AppTy (TyConApp tc []) tys
+
+  -- Then resolve any remaining nullary synonyms.
+  | Just ty' <- tcView ty = Just ty'
 trieMapView _ = Nothing
 
 instance TrieMap TypeMapX where
@@ -820,8 +829,8 @@ instance TrieMap TypeMapX where
 
 instance Eq (DeBruijn Type) where
   env_t@(D env t) == env_t'@(D env' t')
-    | Just new_t  <- coreViewOneStarKind t  = D env new_t == env_t'
-    | Just new_t' <- coreViewOneStarKind t' = env_t       == D env' new_t'
+    | Just new_t  <- tcView t  = D env new_t == env_t'
+    | Just new_t' <- tcView t' = env_t       == D env' new_t'
     | otherwise
     = case (t, t') of
         (CastTy t1 _, _)  -> D env t1 == D env t'
index be72574..91e4285 100644 (file)
@@ -335,7 +335,7 @@ tyConPrimRep1 tc = case tyConPrimRep tc of
 -- of values of types of this kind.
 kindPrimRep :: HasDebugCallStack => SDoc -> Kind -> [PrimRep]
 kindPrimRep doc ki
-  | Just ki' <- coreViewOneStarKind ki
+  | Just ki' <- coreView ki
   = kindPrimRep doc ki'
 kindPrimRep doc (TyConApp typ [runtime_rep])
   = ASSERT( typ `hasKey` tYPETyConKey )
index d5fa275..2428b6d 100644 (file)
@@ -595,8 +595,8 @@ can_eq_nc'
 
 -- Expand synonyms first; see Note [Type synonyms and canonicalization]
 can_eq_nc' flat _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
-  | Just ty1' <- coreView ty1 = can_eq_nc flat ev eq_rel ty1' ps_ty1 ty2  ps_ty2
-  | Just ty2' <- coreView ty2 = can_eq_nc flat ev eq_rel ty1  ps_ty1 ty2' ps_ty2
+  | Just ty1' <- tcView ty1 = can_eq_nc flat ev eq_rel ty1' ps_ty1 ty2  ps_ty2
+  | Just ty2' <- tcView ty2 = can_eq_nc flat ev eq_rel ty1  ps_ty1 ty2' ps_ty2
 
 -- need to check for reflexivity in the ReprEq case.
 -- See Note [Eager reflexivity check]
@@ -1866,8 +1866,8 @@ unifyWanted loc Phantom ty1 ty2
 unifyWanted loc role orig_ty1 orig_ty2
   = go orig_ty1 orig_ty2
   where
-    go ty1 ty2 | Just ty1' <- coreView ty1 = go ty1' ty2
-    go ty1 ty2 | Just ty2' <- coreView ty2 = go ty1 ty2'
+    go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
+    go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
 
     go (FunTy s1 t1) (FunTy s2 t2)
       = do { co_s <- unifyWanted loc role s1 s2
@@ -1917,8 +1917,8 @@ unify_derived _   Phantom _        _        = return ()
 unify_derived loc role    orig_ty1 orig_ty2
   = go orig_ty1 orig_ty2
   where
-    go ty1 ty2 | Just ty1' <- coreView ty1 = go ty1' ty2
-    go ty1 ty2 | Just ty2' <- coreView ty2 = go ty1 ty2'
+    go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
+    go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
 
     go (FunTy s1 t1) (FunTy s2 t2)
       = do { unify_derived loc role s1 s2
index 360142d..2ec11e8 100644 (file)
@@ -2143,7 +2143,7 @@ expandSynonymsToMatch ty1 ty2 = (ty1_ret, ty2_ret)
     --
     -- `tyExpansions (M T10)` returns [Maybe T10] (T10 is not expanded)
     tyExpansions :: Type -> [Type]
-    tyExpansions = unfoldr (\t -> (\x -> (x, x)) `fmap` coreView t)
+    tyExpansions = unfoldr (\t -> (\x -> (x, x)) `fmap` tcView t)
 
     -- | Drop the type pairs until types in a pair look alike (i.e. the outer
     -- constructors are the same).
index 1c54b1b..12bb71c 100644 (file)
@@ -122,7 +122,7 @@ normaliseFfiType' env ty0 = go initRecTc ty0
   where
     go :: RecTcChecker -> Type -> TcM (Coercion, Type, Bag GlobalRdrElt)
     go rec_nts ty
-      | Just ty' <- coreView ty     -- Expand synonyms
+      | Just ty' <- tcView ty     -- Expand synonyms
       = go rec_nts ty'
 
       | Just (tc, tys) <- splitTyConApp_maybe ty
index edf5851..3862839 100644 (file)
@@ -362,7 +362,7 @@ functorLikeTraverse var (FT { ft_triv = caseTrivial,     ft_var = caseVar
        -> Type
        -> (a, Bool)   -- (result of type a, does type contain var)
 
-    go co ty | Just ty' <- coreView ty = go co ty'
+    go co ty | Just ty' <- tcView ty = go co ty'
     go co (TyVarTy    v) | v == var = (if co then caseCoVar else caseVar,True)
     go co (FunTy x y)  | isPredTy x = go co y
                        | xc || yc   = (caseFun xr yr,True)
index c15ac4b..0e3a43c 100644 (file)
@@ -728,7 +728,7 @@ tc_infer_hs_type_ek mode ty ek
 tupKindSort_maybe :: TcKind -> Maybe TupleSort
 tupKindSort_maybe k
   | Just (k', _) <- splitCastTy_maybe k = tupKindSort_maybe k'
-  | Just k'      <- coreView k          = tupKindSort_maybe k'
+  | Just k'      <- tcView k            = tupKindSort_maybe k'
   | isConstraintKind k = Just ConstraintTuple
   | isLiftedTypeKind k = Just BoxedTuple
   | otherwise          = Nothing
index c710fd5..13485d5 100644 (file)
@@ -17,6 +17,7 @@ import TcFlatten
 import TcUnify( canSolveByUnification )
 import VarSet
 import Type
+import Kind( isConstraintKind )
 import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId )
 import CoAxiom( sfInteractTop, sfInteractInert )
 
@@ -31,7 +32,7 @@ import PrelNames ( knownNatClassName, knownSymbolClassName,
                    hasFieldClassName,
                    heqTyConKey, ipClassKey )
 import TysWiredIn ( typeNatKind, typeSymbolKind, heqDataCon,
-                    coercibleDataCon )
+                    coercibleDataCon, constraintKindTyCon )
 import TysPrim    ( eqPrimTyCon, eqReprPrimTyCon )
 import Id( idType, isNaughtyRecordSelector )
 import CoAxiom ( TypeEqn, CoAxiom(..), CoAxBranch(..), fromBranches )
@@ -2405,6 +2406,7 @@ matchTypeable clas [k,t]  -- clas = Typeable
   -- Now cases that do work
   | k `eqType` typeNatKind                 = doTyLit knownNatClassName         t
   | k `eqType` typeSymbolKind              = doTyLit knownSymbolClassName      t
+  | isConstraintKind t                     = doTyConApp clas t constraintKindTyCon []
   | Just (arg,ret) <- splitFunTy_maybe t   = doFunTy    clas t arg ret
   | Just (tc, ks) <- splitTyConApp_maybe t -- See Note [Typeable (T a b c)]
   , onlyNamedBndrsApplied tc ks            = doTyConApp clas t tc ks
index d4e8d4d..783b530 100644 (file)
@@ -168,7 +168,7 @@ module TcType (
   isUnboxedTupleType,   -- Ditto
   isPrimitiveType,
 
-  coreView,
+  tcView, coreView,
 
   tyCoVarsOfType, tyCoVarsOfTypes, closeOverKinds,
   tyCoFVsOfType, tyCoFVsOfTypes,
@@ -799,7 +799,7 @@ instance Outputable TcLevel where
 -- the calls on the RHS are smaller than the LHS
 tcTyFamInsts :: Type -> [(TyCon, [Type])]
 tcTyFamInsts ty
-  | Just exp_ty <- coreView ty  = tcTyFamInsts exp_ty
+  | Just exp_ty <- tcView ty    = tcTyFamInsts exp_ty
 tcTyFamInsts (TyVarTy _)        = []
 tcTyFamInsts (TyConApp tc tys)
   | isTypeFamilyTyCon tc        = [(tc, take (tyConArity tc) tys)]
@@ -855,7 +855,7 @@ exactTyCoVarsOfType :: Type -> TyCoVarSet
 exactTyCoVarsOfType ty
   = go ty
   where
-    go ty | Just ty' <- coreView ty = go ty'  -- This is the key line
+    go ty | Just ty' <- tcView ty = go ty'  -- This is the key line
     go (TyVarTy tv)         = unitVarSet tv `unionVarSet` go (tyVarKind tv)
     go (TyConApp _ tys)     = exactTyCoVarsOfTypes tys
     go (LitTy {})           = emptyVarSet
@@ -1362,7 +1362,7 @@ tcSplitPiTys :: Type -> ([TyBinder], Type)
 tcSplitPiTys = splitPiTys
 
 tcSplitForAllTy_maybe :: Type -> Maybe (TyVarBinder, Type)
-tcSplitForAllTy_maybe ty | Just ty' <- coreView ty = tcSplitForAllTy_maybe ty'
+tcSplitForAllTy_maybe ty | Just ty' <- tcView ty = tcSplitForAllTy_maybe ty'
 tcSplitForAllTy_maybe (ForAllTy tv ty) = Just (tv, ty)
 tcSplitForAllTy_maybe _                = Nothing
 
@@ -1377,14 +1377,14 @@ tcSplitForAllTyVarBndrs = splitForAllTyVarBndrs
 
 -- | Is this a ForAllTy with a named binder?
 tcIsForAllTy :: Type -> Bool
-tcIsForAllTy ty | Just ty' <- coreView ty = tcIsForAllTy ty'
+tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty'
 tcIsForAllTy (ForAllTy {}) = True
 tcIsForAllTy _             = False
 
 tcSplitPredFunTy_maybe :: Type -> Maybe (PredType, Type)
 -- Split off the first predicate argument from a type
 tcSplitPredFunTy_maybe ty
-  | Just ty' <- coreView ty = tcSplitPredFunTy_maybe ty'
+  | Just ty' <- tcView ty = tcSplitPredFunTy_maybe ty'
 tcSplitPredFunTy_maybe (FunTy arg res)
   | isPredTy arg = Just (arg, res)
 tcSplitPredFunTy_maybe _
@@ -1460,7 +1460,7 @@ tcTyConAppTyCon ty
 -- | Like 'tcRepSplitTyConApp_maybe', but only returns the 'TyCon'.
 tcTyConAppTyCon_maybe :: Type -> Maybe TyCon
 tcTyConAppTyCon_maybe ty
-  | Just ty' <- coreView ty = tcTyConAppTyCon_maybe ty'
+  | Just ty' <- tcView ty = tcTyConAppTyCon_maybe ty'
 tcTyConAppTyCon_maybe (TyConApp tc _)
   = Just tc
 tcTyConAppTyCon_maybe (FunTy _ _)
@@ -1478,29 +1478,6 @@ tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
                         Just stuff -> stuff
                         Nothing    -> pprPanic "tcSplitTyConApp" (pprType ty)
 
--- | Split a type constructor application into its type constructor and
--- applied types. Note that this may fail in the case of a 'FunTy' with an
--- argument of unknown kind 'FunTy' (e.g. @FunTy (a :: k) Int@. since the kind
--- of @a@ isn't of the form @TYPE rep@). Consequently, you may need to zonk your
--- type before using this function.
---
--- If you only need the 'TyCon', consider using 'tcTyConAppTyCon_maybe'.
-tcSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
-tcSplitTyConApp_maybe ty | Just ty' <- coreView ty = tcSplitTyConApp_maybe ty'
-tcSplitTyConApp_maybe ty                           = tcRepSplitTyConApp_maybe ty
-
--- | Like 'tcSplitTyConApp_maybe' but doesn't look through type synonyms.
-tcRepSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
-tcRepSplitTyConApp_maybe (TyConApp tc tys)          = Just (tc, tys)
-tcRepSplitTyConApp_maybe (FunTy arg res)
-  | Just arg_rep <- getRuntimeRep_maybe arg
-  , Just res_rep <- getRuntimeRep_maybe res
-  = Just (funTyCon, [arg_rep, res_rep, arg, res])
-
-  | otherwise
-  = pprPanic "tcRepSplitTyConApp_maybe" (ppr arg $$ ppr res)
-tcRepSplitTyConApp_maybe _                          = Nothing
-
 -- | Like 'tcRepSplitTyConApp_maybe', but returns 'Nothing' if,
 --
 -- 1. the type is structurally not a type constructor application, or
@@ -1531,7 +1508,7 @@ tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
                                           (args,res') = tcSplitFunTys res
 
 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
-tcSplitFunTy_maybe ty | Just ty' <- coreView ty         = tcSplitFunTy_maybe ty'
+tcSplitFunTy_maybe ty | Just ty' <- tcView ty         = tcSplitFunTy_maybe ty'
 tcSplitFunTy_maybe (FunTy arg res) | not (isPredTy arg) = Just (arg, res)
 tcSplitFunTy_maybe _                                    = Nothing
         -- Note the typeKind guard
@@ -1580,7 +1557,7 @@ tcFunResultTyN n ty
 
 -----------------------
 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
-tcSplitAppTy_maybe ty | Just ty' <- coreView ty = tcSplitAppTy_maybe ty'
+tcSplitAppTy_maybe ty | Just ty' <- tcView ty = tcSplitAppTy_maybe ty'
 tcSplitAppTy_maybe ty = tcRepSplitAppTy_maybe ty
 
 tcSplitAppTy :: Type -> (Type, Type)
@@ -1598,7 +1575,7 @@ tcSplitAppTys ty
 
 -----------------------
 tcGetTyVar_maybe :: Type -> Maybe TyVar
-tcGetTyVar_maybe ty | Just ty' <- coreView ty = tcGetTyVar_maybe ty'
+tcGetTyVar_maybe ty | Just ty' <- tcView ty = tcGetTyVar_maybe ty'
 tcGetTyVar_maybe (TyVarTy tv)   = Just tv
 tcGetTyVar_maybe _              = Nothing
 
@@ -1606,7 +1583,7 @@ tcGetTyVar :: String -> Type -> TyVar
 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
 
 tcIsTyVarTy :: Type -> Bool
-tcIsTyVarTy ty | Just ty' <- coreView ty = tcIsTyVarTy ty'
+tcIsTyVarTy ty | Just ty' <- tcView ty = tcIsTyVarTy ty'
 tcIsTyVarTy (CastTy ty _) = tcIsTyVarTy ty  -- look through casts, as
                                             -- this is only used for
                                             -- e.g., FlexibleContexts
@@ -1665,8 +1642,8 @@ tcEqType :: TcType -> TcType -> Bool
 -- equality] (in TyCoRep) as `eqType`, but Type.eqType believes (* ==
 -- Constraint), and that is NOT what we want in the type checker!
 tcEqType ty1 ty2
-  = isNothing (tc_eq_type coreView ki1 ki2) &&
-    isNothing (tc_eq_type coreView ty1 ty2)
+  = isNothing (tc_eq_type tcView ki1 ki2) &&
+    isNothing (tc_eq_type tcView ty1 ty2)
   where
     ki1 = typeKind ty1
     ki2 = typeKind ty2
@@ -1675,7 +1652,7 @@ tcEqType ty1 ty2
 -- as long as their non-coercion structure is identical.
 tcEqTypeNoKindCheck :: TcType -> TcType -> Bool
 tcEqTypeNoKindCheck ty1 ty2
-  = isNothing $ tc_eq_type coreView ty1 ty2
+  = isNothing $ tc_eq_type tcView ty1 ty2
 
 -- | Like 'tcEqType', but returns information about whether the difference
 -- is visible in the case of a mismatch.
@@ -1684,7 +1661,7 @@ tcEqTypeNoKindCheck ty1 ty2
 -- @Just False@ : the types differ, and the point of difference is invisible
 tcEqTypeVis :: TcType -> TcType -> Maybe Bool
 tcEqTypeVis ty1 ty2
-  = tc_eq_type coreView ty1 ty2 <!> invis (tc_eq_type coreView ki1 ki2)
+  = tc_eq_type tcView ty1 ty2 <!> invis (tc_eq_type tcView ki1 ki2)
   where
     ki1 = typeKind ty1
     ki2 = typeKind ty2
@@ -1701,7 +1678,7 @@ Just vis       <!> _         = Just vis
 infixr 3 <!>
 
 -- | Real worker for 'tcEqType'. No kind check!
-tc_eq_type :: (TcType -> Maybe TcType)  -- ^ @coreView@, if you want unwrapping
+tc_eq_type :: (TcType -> Maybe TcType)  -- ^ @tcView@, if you want unwrapping
            -> Type -> Type -> Maybe Bool
 tc_eq_type view_fun orig_ty1 orig_ty2 = go True orig_env orig_ty1 orig_ty2
   where
@@ -2060,13 +2037,13 @@ isSigmaTy :: TcType -> Bool
 -- isSigmaTy returns true of any qualified type.  It doesn't
 -- *necessarily* have any foralls.  E.g
 --        f :: (?x::Int) => Int -> Int
-isSigmaTy ty | Just ty' <- coreView ty = isSigmaTy ty'
+isSigmaTy ty | Just ty' <- tcView ty = isSigmaTy ty'
 isSigmaTy (ForAllTy {}) = True
 isSigmaTy (FunTy a _)   = isPredTy a
 isSigmaTy _             = False
 
 isRhoTy :: TcType -> Bool   -- True of TcRhoTypes; see Note [TcRhoType]
-isRhoTy ty | Just ty' <- coreView ty = isRhoTy ty'
+isRhoTy ty | Just ty' <- tcView ty = isRhoTy ty'
 isRhoTy (ForAllTy {}) = False
 isRhoTy (FunTy a r)   = not (isPredTy a) && isRhoTy r
 isRhoTy _             = True
@@ -2079,7 +2056,7 @@ isRhoExpTy (Infer {}) = True
 isOverloadedTy :: Type -> Bool
 -- Yes for a type of a function that might require evidence-passing
 -- Used only by bindLocalMethods
-isOverloadedTy ty | Just ty' <- coreView ty = isOverloadedTy ty'
+isOverloadedTy ty | Just ty' <- tcView ty = isOverloadedTy ty'
 isOverloadedTy (ForAllTy _  ty) = isOverloadedTy ty
 isOverloadedTy (FunTy a _)      = isPredTy a
 isOverloadedTy _                = False
@@ -2163,7 +2140,7 @@ isInsolubleOccursCheck :: EqRel -> TcTyVar -> TcType -> Bool
 isInsolubleOccursCheck eq_rel tv ty
   = go ty
   where
-    go ty | Just ty' <- coreView ty = go ty'
+    go ty | Just ty' <- tcView ty = go ty'
     go (TyVarTy tv') = tv == tv' || go (tyVarKind tv')
     go (LitTy {})    = False
     go (AppTy t1 t2) = go t1 || go t2
@@ -2580,7 +2557,7 @@ sizeType :: Type -> TypeSize
 -- Ignore kinds altogether
 sizeType = go
   where
-    go ty | Just exp_ty <- coreView ty = go exp_ty
+    go ty | Just exp_ty <- tcView ty = go exp_ty
     go (TyVarTy {})              = 1
     go (TyConApp tc tys)
       | isTypeFamilyTyCon tc     = infinity  -- Type-family applications can
index 34bd387..d30a722 100644 (file)
@@ -346,7 +346,7 @@ mkPrimTypeableTodos
 ghcPrimTypeableTyCons :: [TyCon]
 ghcPrimTypeableTyCons = concat
     [ [ runtimeRepTyCon, vecCountTyCon, vecElemTyCon
-      , funTyCon, tupleTyCon Unboxed 0]
+      , funTyCon, tupleTyCon Unboxed 0 ]
     , map (tupleTyCon Unboxed) [2..mAX_TUPLE_SIZE]
     , map sumTyCon [2..mAX_SUM_SIZE]
     , primTyCons
@@ -523,7 +523,7 @@ getKindRep stuff@(Stuff {..}) in_scope = go
     go' :: Kind -> KindRepEnv -> TcRn (LHsExpr Id, KindRepEnv)
     go' k env
         -- Look through type synonyms
-      | Just k' <- coreView k = go' k' env
+      | Just k' <- tcView k = go' k' env
 
         -- We've already generated the needed KindRep
       | Just (id, _) <- lookupTypeMapWithScope env in_scope k
index ef0c95a..6d39169 100644 (file)
@@ -138,7 +138,7 @@ matchExpectedFunTys herald arity orig_ty thing_inside
            ; return (result, idHsWrapper) }
 
     go acc_arg_tys n ty
-      | Just ty' <- coreView ty = go acc_arg_tys n ty'
+      | Just ty' <- tcView ty = go acc_arg_tys n ty'
 
     go acc_arg_tys n (FunTy arg_ty res_ty)
       = ASSERT( not (isPredTy arg_ty) )
@@ -269,7 +269,7 @@ matchActualFunTysPart herald ct_orig mb_thing arity orig_ty
         (tvs, theta, _) = tcSplitSigmaTy ty
 
     go n acc_args ty
-      | Just ty' <- coreView ty = go n acc_args ty'
+      | Just ty' <- tcView ty = go n acc_args ty'
 
     go n acc_args (FunTy arg_ty res_ty)
       = ASSERT( not (isPredTy arg_ty) )
@@ -370,7 +370,7 @@ matchExpectedTyConApp tc orig_ty
   = ASSERT(tc /= funTyCon) go orig_ty
   where
     go ty
-       | Just ty' <- coreView ty
+       | Just ty' <- tcView ty
        = go ty'
 
     go ty@(TyConApp tycon args)
@@ -415,7 +415,7 @@ matchExpectedAppTy orig_ty
   = go orig_ty
   where
     go ty
-      | Just ty' <- coreView ty = go ty'
+      | Just ty' <- tcView ty = go ty'
 
       | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
       = return (mkTcNomReflCo orig_ty, (fun_ty, arg_ty))
@@ -695,8 +695,8 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
               , text "ty_expected =" <+> ppr ty_expected ]
        ; go ty_actual ty_expected }
   where
-    go ty_a ty_e | Just ty_a' <- coreView ty_a = go ty_a' ty_e
-                 | Just ty_e' <- coreView ty_e = go ty_a  ty_e'
+    go ty_a ty_e | Just ty_a' <- tcView ty_a = go ty_a' ty_e
+                 | Just ty_e' <- tcView ty_e = go ty_a  ty_e'
 
     go (TyVarTy tv_a) ty_e
       = do { lookup_res <- lookupTcTyVar tv_a
@@ -1273,8 +1273,8 @@ uType origin t_or_k orig_ty1 orig_ty2
         -- we'll end up saying "can't match Foo with Bool"
         -- rather than "can't match "Int with Bool".  See Trac #4535.
     go ty1 ty2
-      | Just ty1' <- coreView ty1 = go ty1' ty2
-      | Just ty2' <- coreView ty2 = go ty1  ty2'
+      | Just ty1' <- tcView ty1 = go ty1' ty2
+      | Just ty2' <- tcView ty2 = go ty1  ty2'
 
     go (CastTy t1 co1) t2
       = do { co_tys <- go t1 t2
@@ -1768,7 +1768,7 @@ matchExpectedFunKind :: Arity           -- ^ # of args remaining, only for error
                                   -- ^ co :: old_kind ~ arg -> res
 matchExpectedFunKind num_args_remaining ty = go
   where
-    go k | Just k' <- coreView k = go k'
+    go k | Just k' <- tcView k = go k'
 
     go k@(TyVarTy kvar)
       | isTcTyVar kvar, isMetaTyVar kvar
@@ -2040,8 +2040,8 @@ occCheckExpand tv ty
     go env ty@(TyConApp tc tys)
       = case mapM (go env) tys of
           Just tys' -> return (mkTyConApp tc tys')
-          Nothing | Just ty' <- coreView ty -> go env ty'
-                  | otherwise               -> Nothing
+          Nothing | Just ty' <- tcView ty -> go env ty'
+                  | otherwise             -> Nothing
                       -- Failing that, try to expand a synonym
 
     go env (CastTy ty co) =  do { ty' <- go env ty
index a56e7a2..3023dfe 100644 (file)
@@ -518,7 +518,7 @@ check_syn_tc_app env ctxt rank ty tc tys
                 mapM_ check_arg tys
 
           else  -- In the liberal case (only for closed syns), expand then check
-          case coreView ty of
+          case tcView ty of
              Just ty' -> check_type env ctxt rank ty'
              Nothing  -> pprPanic "check_tau_type" (ppr ty)  }
 
@@ -717,7 +717,7 @@ check_pred_help :: Bool    -- True <=> under a type synonym
                 -> DynFlags -> UserTypeCtxt
                 -> PredType -> TcM ()
 check_pred_help under_syn env dflags ctxt pred
-  | Just pred' <- coreView pred  -- Switch on under_syn when going under a
+  | Just pred' <- tcView pred  -- Switch on under_syn when going under a
                                  -- synonym (Trac #9838, yuk)
   = check_pred_help True env dflags ctxt pred'
   | otherwise
@@ -1921,7 +1921,7 @@ checkValidInferredKinds orig_kvs out_of_scope extra
 
 -- Free variables of a type, retaining repetitions, and expanding synonyms
 fvType :: Type -> [TyCoVar]
-fvType ty | Just exp_ty <- coreView ty = fvType exp_ty
+fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
 fvType (TyVarTy tv)          = [tv]
 fvType (TyConApp _ tys)      = fvTypes tys
 fvType (LitTy {})            = []
@@ -1964,7 +1964,7 @@ fvProv (HoleProv h)        = pprPanic "fvProv falls into a hole" (ppr h)
 
 sizeType :: Type -> Int
 -- Size of a type: the number of variables and constructors
-sizeType ty | Just exp_ty <- coreView ty = sizeType exp_ty
+sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
 sizeType (TyVarTy {})      = 1
 sizeType (TyConApp _ tys)  = sizeTypes tys + 1
 sizeType (LitTy {})        = 1
index 5fd17f9..906c697 100644 (file)
@@ -15,12 +15,13 @@ module Kind (
 
         classifiesTypeWithValues,
         isStarKind, isStarKindSynonymTyCon,
+        tcIsStarKind,
         isKindLevPoly
        ) where
 
 #include "HsVersions.h"
 
-import {-# SOURCE #-} Type    ( typeKind, coreViewOneStarKind
+import {-# SOURCE #-} Type    ( typeKind, coreView, tcView
                               , splitTyConApp_maybe )
 import {-# SOURCE #-} DataCon ( DataCon )
 
@@ -98,7 +99,7 @@ isKindLevPoly k = ASSERT2( isStarKind k || _is_type, ppr k )
                       -- the isStarKind check is necessary b/c of Constraint
                   go k
   where
-    go ty | Just ty' <- coreViewOneStarKind ty = go ty'
+    go ty | Just ty' <- coreView ty = go ty'
     go TyVarTy{}         = True
     go AppTy{}           = True  -- it can't be a TyConApp
     go (TyConApp tc tys) = isFamilyTyCon tc || any go tys
@@ -137,13 +138,21 @@ okArrowResultKind = classifiesTypeWithValues
 -- like *, #, TYPE Lifted, TYPE v, Constraint.
 classifiesTypeWithValues :: Kind -> Bool
 -- ^ True of any sub-kind of OpenTypeKind
-classifiesTypeWithValues t | Just t' <- coreViewOneStarKind t = classifiesTypeWithValues t'
+classifiesTypeWithValues t | Just t' <- coreView t = classifiesTypeWithValues t'
 classifiesTypeWithValues (TyConApp tc [_]) = tc `hasKey` tYPETyConKey
 classifiesTypeWithValues _ = False
 
 -- | Is this kind equivalent to *?
+tcIsStarKind :: Kind -> Bool
+tcIsStarKind k | Just k' <- tcView k = isStarKind k'
+tcIsStarKind (TyConApp tc [TyConApp ptr_rep []])
+  =  tc      `hasKey` tYPETyConKey
+  && ptr_rep `hasKey` liftedRepDataConKey
+tcIsStarKind _ = False
+
+-- | Is this kind equivalent to *?
 isStarKind :: Kind -> Bool
-isStarKind k | Just k' <- coreViewOneStarKind k = isStarKind k'
+isStarKind k | Just k' <- coreView k = isStarKind k'
 isStarKind (TyConApp tc [TyConApp ptr_rep []])
   =  tc      `hasKey` tYPETyConKey
   && ptr_rep `hasKey` liftedRepDataConKey
index 5a2431c..37916f4 100644 (file)
@@ -31,6 +31,7 @@ module Type (
         tyConAppTyCon_maybe, tyConAppTyConPicky_maybe,
         tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs,
         splitTyConApp_maybe, splitTyConApp, tyConAppArgN, nextRole,
+        tcRepSplitTyConApp_maybe, tcSplitTyConApp_maybe,
         splitListTyConApp_maybe,
         repSplitTyConApp_maybe,
 
@@ -148,7 +149,7 @@ module Type (
         seqType, seqTypes,
 
         -- * Other views onto Types
-        coreView, coreViewOneStarKind,
+        coreView, tcView,
 
         tyConsOfType,
 
@@ -305,6 +306,18 @@ import Control.Arrow    ( first, second )
                 Type representation
 *                                                                      *
 ************************************************************************
+
+Note [coreView vs tcView]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+So far as the typechecker is concerned, 'Constraint' and 'TYPE LiftedRep' are distinct kinds.
+
+But in Core these two are treated as identical.
+
+We implement this by making 'coreView' convert 'Constraint' to 'TYPE LiftedRep' on the fly.
+The function tcView (used in the type checker) does not do this.
+
+See also Trac #11715, which tracks removing this inconsistency.
+
 -}
 
 {-# INLINE coreView #-}
@@ -312,6 +325,7 @@ coreView :: Type -> Maybe Type
 -- ^ This function Strips off the /top layer only/ of a type synonym
 -- application (if any) its underlying representation type.
 -- Returns Nothing if there is nothing to look through.
+-- This function considers 'Constraint' to be a synonym of @TYPE LiftedRep@.
 --
 -- By being non-recursive and inlined, this case analysis gets efficiently
 -- joined onto the case analysis that the caller is already doing
@@ -323,17 +337,27 @@ coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc t
                -- Its important to use mkAppTys, rather than (foldl AppTy),
                -- because the function part might well return a
                -- partially-applied type constructor; indeed, usually will!
+coreView (TyConApp tc [])
+  | isStarKindSynonymTyCon tc
+  = Just liftedTypeKind
+
 coreView _ = Nothing
 
--- | Like 'coreView', but it also "expands" @Constraint@ to become
--- @TYPE LiftedRep@.
-{-# INLINE coreViewOneStarKind #-}
-coreViewOneStarKind :: Type -> Maybe Type
-coreViewOneStarKind ty
-  | Just ty' <- coreView ty   = Just ty'
-  | TyConApp tc [] <- ty
-  , isStarKindSynonymTyCon tc = Just liftedTypeKind
-  | otherwise                 = Nothing
+-- | Gives the typechecker view of a type. This unwraps synonyms but
+-- leaves 'Constraint' alone. c.f. coreView, which turns Constraint into
+-- TYPE LiftedRep. Returns Nothing if no unwrapping happens.
+-- See also Note [coreView vs tcView] in Type.
+{-# INLINE tcView #-}
+tcView :: Type -> Maybe Type
+tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
+  = Just (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys')
+               -- The free vars of 'rhs' should all be bound by 'tenv', so it's
+               -- ok to use 'substTy' here.
+               -- See also Note [The substitution invariant] in TyCoRep.
+               -- Its important to use mkAppTys, rather than (foldl AppTy),
+               -- because the function part might well return a
+               -- partially-applied type constructor; indeed, usually will!
+tcView _ = Nothing
 
 -----------------------------------------------
 expandTypeSynonyms :: Type -> Type
@@ -702,6 +726,33 @@ tcRepSplitAppTy_maybe (TyConApp tc tys)
   , Just (tys', ty') <- snocView tys
   = Just (TyConApp tc tys', ty')    -- Never create unsaturated type family apps!
 tcRepSplitAppTy_maybe _other = Nothing
+
+-- | Split a type constructor application into its type constructor and
+-- applied types. Note that this may fail in the case of a 'FunTy' with an
+-- argument of unknown kind 'FunTy' (e.g. @FunTy (a :: k) Int@. since the kind
+-- of @a@ isn't of the form @TYPE rep@). Consequently, you may need to zonk your
+-- type before using this function.
+--
+-- If you only need the 'TyCon', consider using 'tcTyConAppTyCon_maybe'.
+tcSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
+-- Defined here to avoid module loops between Unify and TcType.
+tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
+tcSplitTyConApp_maybe ty                         = tcRepSplitTyConApp_maybe ty
+
+-- | Like 'tcSplitTyConApp_maybe' but doesn't look through type synonyms.
+tcRepSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
+-- Defined here to avoid module loops between Unify and TcType.
+tcRepSplitTyConApp_maybe (TyConApp tc tys)          = Just (tc, tys)
+tcRepSplitTyConApp_maybe (FunTy arg res)
+  | Just arg_rep <- getRuntimeRep_maybe arg
+  , Just res_rep <- getRuntimeRep_maybe res
+  = Just (funTyCon, [arg_rep, res_rep, arg, res])
+
+  | otherwise
+  = pprPanic "tcRepSplitTyConApp_maybe" (ppr arg $$ ppr res)
+tcRepSplitTyConApp_maybe _                          = Nothing
+
+
 -------------
 splitAppTy :: Type -> (Type, Type)
 -- ^ Attempts to take a type application apart, as in 'splitAppTy_maybe',
@@ -1995,7 +2046,7 @@ getRuntimeRepFromKind_maybe :: HasDebugCallStack
                             => Type -> Maybe Type
 getRuntimeRepFromKind_maybe = go
   where
-    go k | Just k' <- coreViewOneStarKind k = go k'
+    go k | Just k' <- coreView k = go k'
     go k
       | Just (_tc, [arg]) <- splitTyConApp_maybe k
       = ASSERT2( _tc `hasKey` tYPETyConKey, ppr k )
@@ -2240,8 +2291,8 @@ nonDetCmpTypeX env orig_t1 orig_t2 =
     -- and whether either contains a cast.
     go :: RnEnv2 -> Type -> Type -> TypeOrdering
     go env t1 t2
-      | Just t1' <- coreViewOneStarKind t1 = go env t1' t2
-      | Just t2' <- coreViewOneStarKind t2 = go env t1 t2'
+      | Just t1' <- coreView t1 = go env t1' t2
+      | Just t2' <- coreView t2 = go env t1 t2'
 
     go env (TyVarTy tv1)       (TyVarTy tv2)
       = liftOrdering $ rnOccL env tv1 `nonDetCmpVar` rnOccR env tv2
index e9cc786..be7e4ed 100644 (file)
@@ -15,11 +15,10 @@ piResultTy :: Type -> Type -> Type
 typeKind :: Type -> Kind
 eqType :: Type -> Type -> Bool
 
-coreViewOneStarKind :: Type -> Maybe Type
-
 partitionInvisibles :: TyCon -> (a -> Type) -> [a] -> ([a], [a])
 
 coreView :: Type -> Maybe Type
+tcView :: Type -> Maybe Type
 
 tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
 tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
index 77fe5d8..6dc5f01 100644 (file)
@@ -778,8 +778,9 @@ unify_ty :: Type -> Type  -- Types to be unified and a co
 -- Respects newtypes, PredTypes
 
 unify_ty ty1 ty2 kco
-  | Just ty1' <- coreView ty1 = unify_ty ty1' ty2 kco
-  | Just ty2' <- coreView ty2 = unify_ty ty1 ty2' kco
+    -- TODO: More commentary needed here
+  | Just ty1' <- tcView ty1   = unify_ty ty1' ty2 kco
+  | Just ty2' <- tcView ty2   = unify_ty ty1 ty2' kco
   | CastTy ty1' co <- ty1     = unify_ty ty1' ty2 (co `mkTransCo` kco)
   | CastTy ty2' co <- ty2     = unify_ty ty1 ty2' (kco `mkTransCo` mkSymCo co)
 
@@ -791,9 +792,9 @@ unify_ty ty1 (TyVarTy tv2) kco
          else surelyApart }  -- non-tv on left; tv on right: can't match.
 
 unify_ty ty1 ty2 _kco
-  | Just (tc1, tys1) <- splitTyConApp_maybe ty1
-  , Just (tc2, tys2) <- splitTyConApp_maybe ty2
-  = if tc1 == tc2 || (isStarKind ty1 && isStarKind ty2)
+  | Just (tc1, tys1) <- tcSplitTyConApp_maybe ty1
+  , Just (tc2, tys2) <- tcSplitTyConApp_maybe ty2
+  = if tc1 == tc2 || (tcIsStarKind ty1 && tcIsStarKind ty2)
     then if isInjectiveTyCon tc1 Nominal
          then unify_tys tys1 tys2
          else do { let inj | isTypeFamilyTyCon tc1
@@ -1210,7 +1211,7 @@ ty_co_match :: MatchEnv   -- ^ ambient helpful info
             -> Coercion   -- ^ :: kind of R type of substed ty ~N R kind of co
             -> Maybe LiftCoEnv
 ty_co_match menv subst ty co lkco rkco
-  | Just ty' <- coreViewOneStarKind ty = ty_co_match menv subst ty' co lkco rkco
+  | Just ty' <- coreView ty = ty_co_match menv subst ty' co lkco rkco
 
   -- handle Refl case:
   | tyCoVarsOfType ty `isNotInDomainOf` subst
index ce4ddd3..84346b9 100644 (file)
@@ -19,7 +19,7 @@ Roles12.$tcC2
       Roles12.$trModule
       (GHC.Types.TrNameS "C2"#)
       0
-      GHC.Types.krep$*Arr*
+      $krep
 Roles12.$tc'C:C2
   = GHC.Types.TyCon
       7087988437584478859##
@@ -31,6 +31,9 @@ Roles12.$tc'C:C2
 $krep [InlPrag=[~]] = GHC.Types.KindRepVar 0
 $krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
 $krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun GHC.Types.krep$* $krep
+$krep [InlPrag=[~]]
+  = GHC.Types.KindRepTyConApp GHC.Types.$tcConstraint []
 $krep [InlPrag=[~]]
   = GHC.Types.KindRepTyConApp Roles12.$tcC2 ((:) $krep [])
 Roles12.$trModule
index cc9ce91..11abd0c 100644 (file)
@@ -40,7 +40,7 @@ Roles3.$tcC4
       Roles3.$trModule
       (GHC.Types.TrNameS "C4"#)
       0
-      GHC.Types.krep$*->*->*
+      $krep
 Roles3.$tcC3
   = GHC.Types.TyCon
       5076086601454991970##
@@ -48,7 +48,7 @@ Roles3.$tcC3
       Roles3.$trModule
       (GHC.Types.TrNameS "C3"#)
       0
-      GHC.Types.krep$*->*->*
+      $krep
 Roles3.$tcC2
   = GHC.Types.TyCon
       7902873224172523979##
@@ -56,7 +56,7 @@ Roles3.$tcC2
       Roles3.$trModule
       (GHC.Types.TrNameS "C2"#)
       0
-      GHC.Types.krep$*->*->*
+      $krep
 Roles3.$tc'C:C2
   = GHC.Types.TyCon
       11218882737915989529##
@@ -72,7 +72,7 @@ Roles3.$tcC1
       Roles3.$trModule
       (GHC.Types.TrNameS "C1"#)
       0
-      GHC.Types.krep$*Arr*
+      $krep
 Roles3.$tc'C:C1
   = GHC.Types.TyCon
       4508088879886988796##
@@ -88,6 +88,10 @@ $krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
 $krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
 $krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
 $krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun GHC.Types.krep$* $krep
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun GHC.Types.krep$* $krep
+$krep [InlPrag=[~]]
+  = GHC.Types.KindRepTyConApp GHC.Types.$tcConstraint []
 $krep [InlPrag=[~]]
   = GHC.Types.KindRepTyConApp
       Data.Type.Equality.$tc~
index ac9d08b..69394d2 100644 (file)
@@ -25,7 +25,7 @@ Roles4.$tcC3
       Roles4.$trModule
       (GHC.Types.TrNameS "C3"#)
       0
-      GHC.Types.krep$*Arr*
+      $krep
 Roles4.$tc'C:C3
   = GHC.Types.TyCon
       3133378316178104365##
@@ -41,7 +41,7 @@ Roles4.$tcC1
       Roles4.$trModule
       (GHC.Types.TrNameS "C1"#)
       0
-      GHC.Types.krep$*Arr*
+      $krep
 Roles4.$tc'C:C1
   = GHC.Types.TyCon
       3870707671502302648##
@@ -55,9 +55,12 @@ $krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
 $krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
 $krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
 $krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun GHC.Types.krep$* $krep
 $krep [InlPrag=[~]]
   = GHC.Types.KindRepTyConApp GHC.Types.$tc[] ((:) $krep [])
 $krep [InlPrag=[~]]
+  = GHC.Types.KindRepTyConApp GHC.Types.$tcConstraint []
+$krep [InlPrag=[~]]
   = GHC.Types.KindRepTyConApp Roles4.$tcC3 ((:) $krep [])
 $krep [InlPrag=[~]]
   = GHC.Types.KindRepTyConApp Roles4.$tcC1 ((:) $krep [])
index bb20002..09b9cff 100644 (file)
@@ -43,7 +43,7 @@ T8958.$tcRepresentational
       T8958.$trModule
       (GHC.Types.TrNameS "Representational"#)
       0
-      GHC.Types.krep$*Arr*
+      $krep
 T8958.$tc'C:Representational
   = GHC.Types.TyCon
       2358772282532242424##
@@ -59,7 +59,7 @@ T8958.$tcNominal
       T8958.$trModule
       (GHC.Types.TrNameS "Nominal"#)
       0
-      GHC.Types.krep$*Arr*
+      $krep
 T8958.$tc'C:Nominal
   = GHC.Types.TyCon
       10562260635335201742##
@@ -71,6 +71,7 @@ T8958.$tc'C:Nominal
 $krep [InlPrag=[~]] = GHC.Types.KindRepVar 0
 $krep [InlPrag=[~]] = GHC.Types.KindRepVar 1
 $krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun GHC.Types.krep$* $krep
 $krep [InlPrag=[~]]
   = GHC.Types.KindRepTyConApp
       GHC.Tuple.$tc(,)
@@ -87,6 +88,9 @@ $krep [InlPrag=[~]]
       ((:) @ GHC.Types.KindRep $krep [] @ GHC.Types.KindRep)
 $krep [InlPrag=[~]]
   = GHC.Types.KindRepTyConApp
+      GHC.Types.$tcConstraint [] @ GHC.Types.KindRep
+$krep [InlPrag=[~]]
+  = GHC.Types.KindRepTyConApp
       T8958.$tcRepresentational
       ((:) @ GHC.Types.KindRep $krep [] @ GHC.Types.KindRep)
 $krep [InlPrag=[~]]
diff --git a/testsuite/tests/typecheck/should_run/T11715.hs b/testsuite/tests/typecheck/should_run/T11715.hs
new file mode 100644 (file)
index 0000000..3baeb12
--- /dev/null
@@ -0,0 +1,21 @@
+{-# LANGUAGE AllowAmbiguousTypes, TypeFamilies, TypeOperators #-}
+
+import Data.Kind
+import Data.Typeable
+
+type family F x a b
+type instance F Type       a b = a
+type instance F Constraint a b = b
+
+foo :: x :~: y -> F x a b -> F y a b
+foo Refl = id
+
+unsafeCoerce :: a -> b
+unsafeCoerce x = case eqT :: Maybe (Type :~: Constraint) of
+                   Nothing -> error "No more bug!"
+                   Just r  -> foo r x
+
+main :: IO ()
+main = let x :: Int
+           x = 42
+       in print (unsafeCoerce x :: Double)
diff --git a/testsuite/tests/typecheck/should_run/T11715.stderr b/testsuite/tests/typecheck/should_run/T11715.stderr
new file mode 100644 (file)
index 0000000..6b7b2dd
--- /dev/null
@@ -0,0 +1,3 @@
+T11715: No more bug!
+CallStack (from HasCallStack):
+  error, called at T11715.hs:15:31 in main:Main
index 3c125fe..6e9a28e 100644 (file)
@@ -10,15 +10,15 @@ Bool
 Ordering
 Int -> Int
 Proxy Constraint (Eq Int)
-Proxy Constraint (Int,Int)
+Proxy * (Int,Int)
 Proxy Symbol "hello world"
 Proxy Nat 1
 Proxy [Nat] (': Nat 1 (': Nat 2 (': Nat 3 ('[] Nat))))
 Proxy Ordering 'EQ
-Proxy (RuntimeRep -> Constraint) TYPE
-Proxy Constraint Constraint
-Proxy Constraint Constraint
-Proxy Constraint Constraint
+Proxy (RuntimeRep -> *) TYPE
+Proxy * *
+Proxy * *
+Proxy * *
 Proxy RuntimeRep 'LiftedRep
 Proxy (Nat,Symbol) ('(,) Nat Symbol 1 "hello")
-Proxy (Constraint -> Constraint -> Constraint) (~~ Constraint Constraint)
+Proxy (* -> * -> Constraint) (~~ * *)
index 8f5d3fb..46cb8e4 100644 (file)
@@ -15,14 +15,14 @@ Int#
 (##)
 (#,#) 'IntRep 'LiftedRep Int# Int
 Proxy Constraint (Eq Int)
-Proxy Constraint (Int,Int)
+Proxy * (Int,Int)
 Proxy Symbol "hello world"
 Proxy Nat 1
 Proxy [Nat] (': Nat 1 (': Nat 2 (': Nat 3 ('[] Nat))))
 Proxy Ordering 'EQ
-Proxy (RuntimeRep -> Constraint) TYPE
-Proxy Constraint Constraint
-Proxy Constraint Constraint
-Proxy Constraint Constraint
+Proxy (RuntimeRep -> *) TYPE
+Proxy * *
+Proxy * *
+Proxy * *
 Proxy RuntimeRep 'LiftedRep
 RealWorld
index 60b5fae..0690f67 100755 (executable)
@@ -121,3 +121,4 @@ test('TestTypeableBinary', normal, compile_and_run, [''])
 test('Typeable1', normal, compile_fail, [''])
 test('TypeableEq', normal, compile_and_run, [''])
 test('T13435', normal, compile_and_run, [''])
+test('T11715', exit_code(1), compile_and_run, [''])