Commit 6575f4b6 authored by Ben Gamari's avatar Ben Gamari 🐢

Clean up coreView/tcView.

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
parent 29645274
......@@ -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'
......
......@@ -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 )
......
......@@ -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
......
......@@ -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).
......
......@@ -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
......
......@@ -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)
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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]
......
</
......@@ -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