summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/coreSyn/CoreFVs.hs1
-rw-r--r--compiler/coreSyn/CoreLint.hs33
-rw-r--r--compiler/coreSyn/CoreSubst.hs4
-rw-r--r--compiler/coreSyn/TrieMap.hs6
-rw-r--r--compiler/iface/ToIface.hs6
-rw-r--r--compiler/prelude/TysPrim.hs27
-rw-r--r--compiler/specialise/Rules.hs6
-rw-r--r--compiler/typecheck/TcCanonical.hs47
-rw-r--r--compiler/typecheck/TcSMonad.hs2
-rw-r--r--compiler/typecheck/TcTyDecls.hs1
-rw-r--r--compiler/typecheck/TcType.hs98
-rw-r--r--compiler/typecheck/TcUnify.hs3
-rw-r--r--compiler/typecheck/TcValidity.hs1
-rw-r--r--compiler/types/Coercion.hs118
-rw-r--r--compiler/types/Coercion.hs-boot6
-rw-r--r--compiler/types/FamInstEnv.hs1
-rw-r--r--compiler/types/OptCoercion.hs9
-rw-r--r--compiler/types/TyCoRep.hs13
-rw-r--r--compiler/types/TyCon.hs4
-rw-r--r--compiler/types/Type.hs156
-rw-r--r--compiler/types/Unify.hs20
21 files changed, 464 insertions, 98 deletions
diff --git a/compiler/coreSyn/CoreFVs.hs b/compiler/coreSyn/CoreFVs.hs
index eba64cdb56..3a90ea0f03 100644
--- a/compiler/coreSyn/CoreFVs.hs
+++ b/compiler/coreSyn/CoreFVs.hs
@@ -373,6 +373,7 @@ orphNamesOfCo (TyConAppCo _ tc cos) = unitNameSet (getName tc) `unionNameSet` or
orphNamesOfCo (AppCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
orphNamesOfCo (ForAllCo _ kind_co co)
= orphNamesOfCo kind_co `unionNameSet` orphNamesOfCo co
+orphNamesOfCo (FunCo _ co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
orphNamesOfCo (CoVarCo _) = emptyNameSet
orphNamesOfCo (AxiomInstCo con _ cos) = orphNamesOfCoCon con `unionNameSet` orphNamesOfCos cos
orphNamesOfCo (UnivCo p _ t1 t2) = orphNamesOfProv p `unionNameSet` orphNamesOfType t1 `unionNameSet` orphNamesOfType t2
diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index 053ac21d15..2f34046d6a 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -130,6 +130,12 @@ Outstanding issues:
-- may well be happening...);
+Note [Linting function types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+As described in Note [Representation of function types], all saturated
+applications of funTyCon are represented with the FunTy constructor. We check
+this invariant in lintType.
+
Note [Linting type lets]
~~~~~~~~~~~~~~~~~~~~~~~~
In the desugarer, it's very very convenient to be able to say (in effect)
@@ -1245,6 +1251,13 @@ lintType ty@(TyConApp tc tys)
= lintType ty' -- Expand type synonyms, so that we do not bogusly complain
-- about un-saturated type synonyms
+ -- We should never see a saturated application of funTyCon; such applications
+ -- should be represented with the FunTy constructor. See Note [Linting
+ -- function types] and Note [Representation of function types].
+ | isFunTyCon tc
+ , length tys == 4
+ = failWithL (hang (text "Saturated application of (->)") 2 (ppr ty))
+
| isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
-- Also type synonyms and type families
, length tys < tyConArity tc
@@ -1487,14 +1500,9 @@ lintCoercion (Refl r ty)
lintCoercion co@(TyConAppCo r tc cos)
| tc `hasKey` funTyConKey
- , [co1,co2] <- cos
- = do { (k1,k'1,s1,t1,r1) <- lintCoercion co1
- ; (k2,k'2,s2,t2,r2) <- lintCoercion co2
- ; k <- lintArrow (text "coercion" <+> quotes (ppr co)) k1 k2
- ; k' <- lintArrow (text "coercion" <+> quotes (ppr co)) k'1 k'2
- ; lintRole co1 r r1
- ; lintRole co2 r r2
- ; return (k, k', mkFunTy s1 s2, mkFunTy t1 t2, r) }
+ , [_rep1,_rep2,_co1,_co2] <- cos
+ = do { failWithL (text "Saturated TyConAppCo (->):" <+> ppr co)
+ } -- All saturated TyConAppCos should be FunCos
| Just {} <- synTyConDefn_maybe tc
= failWithL (text "Synonym in TyConAppCo:" <+> ppr co)
@@ -1545,6 +1553,15 @@ lintCoercion (ForAllCo tv1 kind_co co)
substTy subst t2
; return (k3, k4, tyl, tyr, r) } }
+lintCoercion co@(FunCo r co1 co2)
+ = do { (k1,k'1,s1,t1,r1) <- lintCoercion co1
+ ; (k2,k'2,s2,t2,r2) <- lintCoercion co2
+ ; k <- lintArrow (text "coercion" <+> quotes (ppr co)) k1 k2
+ ; k' <- lintArrow (text "coercion" <+> quotes (ppr co)) k'1 k'2
+ ; lintRole co1 r r1
+ ; lintRole co2 r r2
+ ; return (k, k', mkFunTy s1 s2, mkFunTy t1 t2, r) }
+
lintCoercion (CoVarCo cv)
| not (isCoVar cv)
= failWithL (hang (text "Bad CoVarCo:" <+> ppr cv)
diff --git a/compiler/coreSyn/CoreSubst.hs b/compiler/coreSyn/CoreSubst.hs
index d669569d18..89a92f886a 100644
--- a/compiler/coreSyn/CoreSubst.hs
+++ b/compiler/coreSyn/CoreSubst.hs
@@ -1678,7 +1678,7 @@ pushCoValArg co
= Just (mkRepReflCo arg, mkRepReflCo res)
| isFunTy tyL
- , [co1, co2] <- decomposeCo 2 co
+ , [_, _, co1, co2] <- decomposeCo 4 co
-- If co :: (tyL1 -> tyL2) ~ (tyR1 -> tyR2)
-- then co1 :: tyL1 ~ tyR1
-- co2 :: tyL2 ~ tyR2
@@ -1702,7 +1702,7 @@ pushCoercionIntoLambda in_scope x e co
, Pair s1s2 t1t2 <- coercionKind co
, Just (_s1,_s2) <- splitFunTy_maybe s1s2
, Just (t1,_t2) <- splitFunTy_maybe t1t2
- = let [co1, co2] = decomposeCo 2 co
+ = let [_rep1, _rep2, co1, co2] = decomposeCo 4 co
-- Should we optimize the coercions here?
-- Otherwise they might not match too well
x' = x `setIdType` t1
diff --git a/compiler/coreSyn/TrieMap.hs b/compiler/coreSyn/TrieMap.hs
index 4a6e2452fd..710d80d251 100644
--- a/compiler/coreSyn/TrieMap.hs
+++ b/compiler/coreSyn/TrieMap.hs
@@ -796,9 +796,9 @@ data TypeMapX a
-- to nested AppTys. Why the last one? See Note [Equality on AppTys] in Type
trieMapView :: Type -> Maybe Type
trieMapView ty | Just ty' <- coreViewOneStarKind ty = Just ty'
-trieMapView (TyConApp tc tys@(_:_)) = Just $ foldl AppTy (TyConApp tc []) tys
-trieMapView (FunTy arg res)
- = Just ((TyConApp funTyCon [] `AppTy` arg) `AppTy` res)
+trieMapView ty
+ | Just (tc, tys@(_:_)) <- splitTyConApp_maybe ty
+ = Just $ foldl AppTy (TyConApp tc []) tys
trieMapView _ = Nothing
instance TrieMap TypeMapX where
diff --git a/compiler/iface/ToIface.hs b/compiler/iface/ToIface.hs
index 37d41f4393..c0229b8e62 100644
--- a/compiler/iface/ToIface.hs
+++ b/compiler/iface/ToIface.hs
@@ -201,9 +201,9 @@ toIfaceTyLit (StrTyLit x) = IfaceStrTyLit x
----------------
toIfaceCoercion :: Coercion -> IfaceCoercion
toIfaceCoercion (Refl r ty) = IfaceReflCo r (toIfaceType ty)
-toIfaceCoercion (TyConAppCo r tc cos)
+toIfaceCoercion co@(TyConAppCo r tc cos)
| tc `hasKey` funTyConKey
- , [arg,res] <- cos = IfaceFunCo r (toIfaceCoercion arg) (toIfaceCoercion res)
+ , [_,_,_,_] <- cos = pprPanic "toIfaceCoercion" (ppr co)
| otherwise = IfaceTyConAppCo r (toIfaceTyCon tc)
(map toIfaceCoercion cos)
toIfaceCoercion (AppCo co1 co2) = IfaceAppCo (toIfaceCoercion co1)
@@ -211,6 +211,8 @@ toIfaceCoercion (AppCo co1 co2) = IfaceAppCo (toIfaceCoercion co1)
toIfaceCoercion (ForAllCo tv k co) = IfaceForAllCo (toIfaceTvBndr tv)
(toIfaceCoercion k)
(toIfaceCoercion co)
+toIfaceCoercion (FunCo r co1 co2) = IfaceFunCo r (toIfaceCoercion co1)
+ (toIfaceCoercion co2)
toIfaceCoercion (CoVarCo cv) = IfaceCoVarCo (toIfaceCoVar cv)
toIfaceCoercion (AxiomInstCo con ind cos)
= IfaceAxiomInstCo (coAxiomName con) ind
diff --git a/compiler/prelude/TysPrim.hs b/compiler/prelude/TysPrim.hs
index df8a380b83..cdc25e0fc6 100644
--- a/compiler/prelude/TysPrim.hs
+++ b/compiler/prelude/TysPrim.hs
@@ -24,7 +24,7 @@ module TysPrim(
openAlphaTy, openBetaTy, openAlphaTyVar, openBetaTyVar,
-- Kind constructors...
- tYPETyConName,
+ tYPETyCon, tYPETyConName,
-- Kinds
tYPE, primRepToRuntimeRep,
@@ -94,7 +94,7 @@ import {-# SOURCE #-} TysWiredIn
, doubleElemRepDataConTy
, mkPromotedListTy )
-import Var ( TyVar, mkTyVar )
+import Var ( TyVar, TyVarBndr(TvBndr), mkTyVar )
import Name
import TyCon
import SrcLoc
@@ -328,20 +328,21 @@ openBetaTy = mkTyVarTy openBetaTyVar
funTyConName :: Name
funTyConName = mkPrimTyConName (fsLit "(->)") funTyConKey funTyCon
+-- | The @(->)@ type constructor.
+--
+-- @
+-- (->) :: forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep).
+-- TYPE rep1 -> TYPE rep2 -> *
+-- @
funTyCon :: TyCon
funTyCon = mkFunTyCon funTyConName tc_bndrs tc_rep_nm
where
- tc_bndrs = mkTemplateAnonTyConBinders [liftedTypeKind, liftedTypeKind]
-
- -- You might think that (->) should have type (?? -> ? -> *), and you'd be right
- -- But if we do that we get kind errors when saying
- -- instance Control.Arrow (->)
- -- because the expected kind is (*->*->*). The trouble is that the
- -- expected/actual stuff in the unifier does not go contra-variant, whereas
- -- the kind sub-typing does. Sigh. It really only matters if you use (->) in
- -- a prefix way, thus: (->) Int# Int#. And this is unusual.
- -- because they are never in scope in the source
-
+ tc_bndrs = [ TvBndr runtimeRep1TyVar (NamedTCB Inferred)
+ , TvBndr runtimeRep2TyVar (NamedTCB Inferred)
+ ]
+ ++ mkTemplateAnonTyConBinders [ tYPE runtimeRep1Ty
+ , tYPE runtimeRep2Ty
+ ]
tc_rep_nm = mkPrelTyConRepName funTyConName
{-
diff --git a/compiler/specialise/Rules.hs b/compiler/specialise/Rules.hs
index 168104156f..ae0798ac2b 100644
--- a/compiler/specialise/Rules.hs
+++ b/compiler/specialise/Rules.hs
@@ -810,6 +810,12 @@ match_co renv subst co1 co2
| tc1 == tc2
-> match_cos renv subst cos1 cos2
_ -> Nothing
+match_co renv subst co1 co2
+ | Just (arg1, res1) <- splitFunCo_maybe co1
+ = case splitFunCo_maybe co2 of
+ Just (arg2, res2)
+ -> match_cos renv subst [arg1, res1] [arg2, res2]
+ _ -> Nothing
match_co _ _ _co1 _co2
-- Currently just deals with CoVarCo, TyConAppCo and Refl
#ifdef DEBUG
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 038b6b9914..c6682081db 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -33,6 +33,7 @@ import Util
import Bag
import MonadUtils
import Control.Monad
+import Data.Maybe ( isJust )
import Data.List ( zip4, foldl' )
import BasicTypes
@@ -540,6 +541,25 @@ track whether or not we've already flattened.
It is conceivable to do a better job at tracking whether or not a type
is flattened, but this is left as future work. (Mar '15)
+
+
+Note [FunTy and decomposing tycon applications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+When can_eq_nc' attempts to decompose a tycon application we haven't yet zonked.
+This means that we may very well have a FunTy containing a type of some unknown
+kind. For instance, we may have,
+
+ FunTy (a :: k) Int
+
+Where k is a unification variable. tcRepSplitTyConApp_maybe panics in the event
+that it sees such a type as it cannot determine the RuntimeReps which the (->)
+is applied to. Consequently, it is vital that we instead use
+tcRepSplitTyConApp_maybe', which simply returns Nothing in such a case.
+
+When this happens can_eq_nc' will fail to decompose, zonk, and try again.
+Zonking should fill the variable k, meaning that decomposition will succeed the
+second time around.
-}
canEqNC :: CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
@@ -613,8 +633,9 @@ can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
-- Try to decompose type constructor applications
-- Including FunTy (s -> t)
can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1 _ ty2 _
- | Just (tc1, tys1) <- tcRepSplitTyConApp_maybe ty1
- , Just (tc2, tys2) <- tcRepSplitTyConApp_maybe ty2
+ --- See Note [FunTy and decomposing type constructor applications].
+ | Just (tc1, tys1) <- tcRepSplitTyConApp_maybe' ty1
+ , Just (tc2, tys2) <- tcRepSplitTyConApp_maybe' ty2
, not (isTypeFamilyTyCon tc1)
, not (isTypeFamilyTyCon tc2)
= canTyConApp ev eq_rel tc1 tys1 tc2 tys2
@@ -696,6 +717,26 @@ zonk_eq_types = go
go (TyVarTy tv1) ty2 = tyvar NotSwapped tv1 ty2
go ty1 (TyVarTy tv2) = tyvar IsSwapped tv2 ty1
+ -- We handle FunTys explicitly here despite the fact that they could also be
+ -- treated as an application. Why? Well, for one it's cheaper to just look
+ -- at two types (the argument and result types) than four (the argument,
+ -- result, and their RuntimeReps). Also, we haven't completely zonked yet,
+ -- so we may run into an unzonked type variable while trying to compute the
+ -- RuntimeReps of the argument and result types. This can be observed in
+ -- testcase tc269.
+ go ty1 ty2
+ | Just (arg1, res1) <- split1
+ , Just (arg2, res2) <- split2
+ = do { res_a <- go arg1 arg2
+ ; res_b <- go res1 res2
+ ; return $ combine_rev mkFunTy res_b res_a
+ }
+ | isJust split1 || isJust split2
+ = bale_out ty1 ty2
+ where
+ split1 = tcSplitFunTy_maybe ty1
+ split2 = tcSplitFunTy_maybe ty2
+
go ty1 ty2
| Just (tc1, tys1) <- tcRepSplitTyConApp_maybe ty1
, Just (tc2, tys2) <- tcRepSplitTyConApp_maybe ty2
@@ -1830,7 +1871,7 @@ unifyWanted loc role orig_ty1 orig_ty2
go (FunTy s1 t1) (FunTy s2 t2)
= do { co_s <- unifyWanted loc role s1 s2
; co_t <- unifyWanted loc role t1 t2
- ; return (mkTyConAppCo role funTyCon [co_s,co_t]) }
+ ; return (mkFunCo role co_s co_t) }
go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
| tc1 == tc2, tys1 `equalLength` tys2
, isInjectiveTyCon tc1 role -- don't look under newtypes at Rep equality
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 14cb9f20bb..19186c2528 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -284,7 +284,7 @@ extendWorkListCt :: Ct -> WorkList -> WorkList
extendWorkListCt ct wl
= case classifyPredType (ctPred ct) of
EqPred NomEq ty1 _
- | Just (tc,_) <- tcSplitTyConApp_maybe ty1
+ | Just tc <- tcTyConAppTyCon_maybe ty1
, isTypeFamilyTyCon tc
-> extendWorkListFunEq ct wl
diff --git a/compiler/typecheck/TcTyDecls.hs b/compiler/typecheck/TcTyDecls.hs
index 7b69bad264..96154cca8b 100644
--- a/compiler/typecheck/TcTyDecls.hs
+++ b/compiler/typecheck/TcTyDecls.hs
@@ -113,6 +113,7 @@ synonymTyConsOfType ty
go_co (TyConAppCo _ tc cs) = go_tc tc `plusNameEnv` go_co_s cs
go_co (AppCo co co') = go_co co `plusNameEnv` go_co co'
go_co (ForAllCo _ co co') = go_co co `plusNameEnv` go_co co'
+ go_co (FunCo _ co co') = go_co co `plusNameEnv` go_co co'
go_co (CoVarCo _) = emptyNameEnv
go_co (AxiomInstCo _ _ cs) = go_co_s cs
go_co (UnivCo p _ ty ty') = go_prov p `plusNameEnv` go ty `plusNameEnv` go ty'
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index a0ca0b2555..7a87a18939 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -62,8 +62,9 @@ module TcType (
tcSplitPhiTy, tcSplitPredFunTy_maybe,
tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcFunResultTyN,
tcSplitFunTysN,
- tcSplitTyConApp, tcSplitTyConApp_maybe, tcRepSplitTyConApp_maybe,
- tcTyConAppTyCon, tcTyConAppArgs,
+ tcSplitTyConApp, tcSplitTyConApp_maybe,
+ tcRepSplitTyConApp_maybe, tcRepSplitTyConApp_maybe',
+ tcTyConAppTyCon, tcTyConAppTyCon_maybe, tcTyConAppArgs,
tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcRepSplitAppTy_maybe,
tcGetTyVar_maybe, tcGetTyVar, nextRole,
tcSplitSigmaTy, tcSplitNestedSigmaTys, tcDeepSplitSigmaTy_maybe,
@@ -862,6 +863,7 @@ exactTyCoVarsOfType ty
goCo (AppCo co arg) = goCo co `unionVarSet` goCo arg
goCo (ForAllCo tv k_co co)
= goCo co `delVarSet` tv `unionVarSet` goCo k_co
+ goCo (FunCo _ co1 co2) = goCo co1 `unionVarSet` goCo co2
goCo (CoVarCo v) = unitVarSet v `unionVarSet` go (varType v)
goCo (AxiomInstCo _ _ args) = goCos args
goCo (UnivCo p _ t1 t2) = goProv p `unionVarSet` go t1 `unionVarSet` go t2
@@ -1420,9 +1422,21 @@ tcDeepSplitSigmaTy_maybe ty
-----------------------
tcTyConAppTyCon :: Type -> TyCon
-tcTyConAppTyCon ty = case tcSplitTyConApp_maybe ty of
- Just (tc, _) -> tc
- Nothing -> pprPanic "tcTyConAppTyCon" (pprType ty)
+tcTyConAppTyCon ty
+ = case tcTyConAppTyCon_maybe ty of
+ Just tc -> tc
+ Nothing -> pprPanic "tcTyConAppTyCon" (pprType ty)
+
+-- | Like 'tcRepSplitTyConApp_maybe', but only returns the 'TyCon'.
+tcTyConAppTyCon_maybe :: Type -> Maybe TyCon
+tcTyConAppTyCon_maybe ty
+ | Just ty' <- coreView ty = tcTyConAppTyCon_maybe ty'
+tcTyConAppTyCon_maybe (TyConApp tc _)
+ = Just tc
+tcTyConAppTyCon_maybe (FunTy _ _)
+ = Just funTyCon
+tcTyConAppTyCon_maybe _
+ = Nothing
tcTyConAppArgs :: Type -> [Type]
tcTyConAppArgs ty = case tcSplitTyConApp_maybe ty of
@@ -1434,14 +1448,48 @@ tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
Just stuff -> stuff
Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
-tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
+-- | 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
-tcRepSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
-tcRepSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
-tcRepSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
-tcRepSplitTyConApp_maybe _ = Nothing
+-- | 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
+--
+-- 2. the type is a function type (e.g. application of 'funTyCon'), but we
+-- currently don't even enough information to fully determine its RuntimeRep
+-- variables. For instance, @FunTy (a :: k) Int@.
+--
+-- By constrast 'tcRepSplitTyConApp_maybe' panics in the second case.
+--
+-- The behavior here is needed during canonicalization; see Note [FunTy and
+-- decomposing tycon applications] in TcCanonical for details.
+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])
+tcRepSplitTyConApp_maybe' _ = Nothing
-----------------------
@@ -1627,6 +1675,7 @@ tc_eq_type :: (TcType -> Maybe TcType) -- ^ @coreView@, 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
+ go :: Bool -> RnEnv2 -> Type -> Type -> Maybe Bool
go vis env t1 t2 | Just t1' <- view_fun t1 = go vis env t1' t2
go vis env t1 t2 | Just t2' <- view_fun t2 = go vis env t1 t2'
@@ -1641,8 +1690,15 @@ tc_eq_type view_fun orig_ty1 orig_ty2 = go True orig_env orig_ty1 orig_ty2
= go (isVisibleArgFlag vis1) env (tyVarKind tv1) (tyVarKind tv2)
<!> go vis (rnBndr2 env tv1 tv2) ty1 ty2
<!> check vis (vis1 == vis2)
+ -- Make sure we handle all FunTy cases since falling through to the
+ -- AppTy case means that tcRepSplitAppTy_maybe may see an unzonked
+ -- kind variable, which causes things to blow up.
go vis env (FunTy arg1 res1) (FunTy arg2 res2)
= go vis env arg1 arg2 <!> go vis env res1 res2
+ go vis env ty (FunTy arg res)
+ = eqFunTy vis env arg res ty
+ go vis env (FunTy arg res) ty
+ = eqFunTy vis env arg res ty
-- See Note [Equality on AppTys] in Type
go vis env (AppTy s1 t1) ty2
@@ -1679,6 +1735,28 @@ tc_eq_type view_fun orig_ty1 orig_ty2 = go True orig_env orig_ty1 orig_ty2
orig_env = mkRnEnv2 $ mkInScopeSet $ tyCoVarsOfTypes [orig_ty1, orig_ty2]
+ -- @eqFunTy arg res ty@ is True when @ty@ equals @FunTy arg res@. This is
+ -- sometimes hard to know directly because @ty@ might have some casts
+ -- obscuring the FunTy. And 'splitAppTy' is difficult because we can't
+ -- always extract a RuntimeRep (see Note [xyz]) if the kind of the arg or
+ -- res is unzonked/unflattened. Thus this function, which handles this
+ -- corner case.
+ eqFunTy :: Bool -> RnEnv2 -> Type -> Type -> Type -> Maybe Bool
+ eqFunTy vis env arg res (FunTy arg' res')
+ = go vis env arg arg' <!> go vis env res res'
+ eqFunTy vis env arg res ty@(AppTy{})
+ | Just (tc, [_, _, arg', res']) <- get_args ty []
+ , tc == funTyCon
+ = go vis env arg arg' <!> go vis env res res'
+ where
+ get_args :: Type -> [Type] -> Maybe (TyCon, [Type])
+ get_args (AppTy f x) args = get_args f (x:args)
+ get_args (CastTy t _) args = get_args t args
+ get_args (TyConApp tc tys) args = Just (tc, tys ++ args)
+ get_args _ _ = Nothing
+ eqFunTy vis _ _ _ _
+ = Just vis
+
-- | Like 'pickyEqTypeVis', but returns a Bool for convenience
pickyEqType :: TcType -> TcType -> Bool
-- Check when two types _look_ the same, _including_ synonyms.
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index db3233e26f..75732c6f05 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -2071,6 +2071,9 @@ occCheckExpand tv ty
env' = extendVarEnv env tv' tv''
; body' <- go_co env' body_co
; return (ForAllCo tv'' kind_co' body') }
+ go_co env (FunCo r co1 co2) = do { co1' <- go_co env co1
+ ; co2' <- go_co env co2
+ ; return (mkFunCo r co1' co2') }
go_co env (CoVarCo c) = do { k' <- go env (varType c)
; return (mkCoVarCo (setVarType c k')) }
go_co env (AxiomInstCo ax ind args) = do { args' <- mapM (go_co env) args
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index fb6bb60fd0..f7cb3197ef 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -1900,6 +1900,7 @@ fvCo (Refl _ ty) = fvType ty
fvCo (TyConAppCo _ _ args) = concatMap fvCo args
fvCo (AppCo co arg) = fvCo co ++ fvCo arg
fvCo (ForAllCo tv h co) = filter (/= tv) (fvCo co) ++ fvCo h
+fvCo (FunCo _ co1 co2) = fvCo co1 ++ fvCo co2
fvCo (CoVarCo v) = [v]
fvCo (AxiomInstCo _ _ args) = concatMap fvCo args
fvCo (UnivCo p _ t1 t2) = fvProv p ++ fvType t1 ++ fvType t2
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index c7debd4d6f..f5791457ac 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -2,7 +2,7 @@
(c) The University of Glasgow 2006
-}
-{-# LANGUAGE RankNTypes, CPP, MultiWayIf #-}
+{-# LANGUAGE RankNTypes, CPP, MultiWayIf, FlexibleContexts #-}
-- | Module for (a) type kinds and (b) type coercions,
-- as used in System FC. See 'CoreSyn.Expr' for
@@ -51,6 +51,7 @@ module Coercion (
decomposeCo, getCoVar_maybe,
splitTyConAppCo_maybe,
splitAppCo_maybe,
+ splitFunCo_maybe,
splitForAllCo_maybe,
nthRole, tyConRolesX, tyConRolesRepresentational, setNominalRole_maybe,
@@ -107,6 +108,7 @@ module Coercion (
import TyCoRep
import Type
+import Kind
import TyCon
import CoAxiom
import Var
@@ -114,12 +116,14 @@ import VarEnv
import Name hiding ( varName )
import Util
import BasicTypes
+import FastString
import Outputable
import Unique
import Pair
import SrcLoc
import PrelNames
import TysPrim ( eqPhantPrimTyCon )
+import {-# SOURCE #-} TysWiredIn ( constraintKind )
import ListSetOps
import Maybes
import UniqFM
@@ -174,13 +178,11 @@ pprParendCo co = ppr_co TyConPrec co
ppr_co :: TyPrec -> Coercion -> SDoc
ppr_co _ (Refl r ty) = angleBrackets (ppr ty) <> ppr_role r
-ppr_co p co@(TyConAppCo _ tc [_,_])
- | tc `hasKey` funTyConKey = ppr_fun_co p co
-
ppr_co _ (TyConAppCo r tc cos) = pprTcAppCo TyConPrec ppr_co tc cos <> ppr_role r
ppr_co p (AppCo co arg) = maybeParen p TyConPrec $
pprCo co <+> ppr_co TyConPrec arg
ppr_co p co@(ForAllCo {}) = ppr_forall_co p co
+ppr_co p co@(FunCo {}) = ppr_fun_co p co
ppr_co _ (CoVarCo cv) = parenSymOcc (getOccName cv) (ppr cv)
ppr_co p (AxiomInstCo con index args)
= pprPrefixApp p (ppr (getName con) <> brackets (ppr index))
@@ -237,8 +239,7 @@ ppr_fun_co :: TyPrec -> Coercion -> SDoc
ppr_fun_co p co = pprArrowChain p (split co)
where
split :: Coercion -> [SDoc]
- split (TyConAppCo _ f [arg, res])
- | f `hasKey` funTyConKey
+ split (FunCo _ arg res)
= ppr_co FunPrec arg : split res
split co = [ppr_co TopPrec co]
@@ -319,6 +320,8 @@ splitTyConAppCo_maybe (Refl r ty)
; let args = zipWith mkReflCo (tyConRolesX r tc) tys
; return (tc, args) }
splitTyConAppCo_maybe (TyConAppCo _ tc cos) = Just (tc, cos)
+splitTyConAppCo_maybe (FunCo _ arg res) = Just (funTyCon, cos)
+ where cos = [mkRuntimeRepCo arg, mkRuntimeRepCo res, arg, res]
splitTyConAppCo_maybe _ = Nothing
-- first result has role equal to input; third result is Nominal
@@ -339,6 +342,10 @@ splitAppCo_maybe (Refl r ty)
= Just (mkReflCo r ty1, mkNomReflCo ty2)
splitAppCo_maybe _ = Nothing
+splitFunCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
+splitFunCo_maybe (FunCo _ arg res) = Just (arg, res)
+splitFunCo_maybe _ = Nothing
+
splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
splitForAllCo_maybe (ForAllCo tv k_co co) = Just (tv, k_co, co)
splitForAllCo_maybe _ = Nothing
@@ -397,6 +404,46 @@ mkHeteroCoercionType Nominal = mkHeteroPrimEqPred
mkHeteroCoercionType Representational = mkHeteroReprPrimEqPred
mkHeteroCoercionType Phantom = panic "mkHeteroCoercionType"
+constraintIsLifted :: CoAxiomRule
+constraintIsLifted =
+ CoAxiomRule { coaxrName = mkFastString "constraintIsLifted"
+ , coaxrAsmpRoles = []
+ , coaxrRole = Nominal
+ , coaxrProves =
+ const $ Just $ Pair constraintKind liftedTypeKind
+ }
+
+-- | Given a coercion @co1 :: (a :: TYPE r1) ~ (b :: TYPE r2)@,
+-- produce a coercion @rep_co :: r1 ~ r2@.
+mkRuntimeRepCo :: Coercion -> Coercion
+mkRuntimeRepCo co
+ -- This is currently a bit tricky since we can see types of kind Constraint
+ -- in addition to the usual things of kind (TYPE rep). We first map
+ -- Constraint-kinded types to (TYPE 'LiftedRep).
+ -- FIXME: this is terrible
+ | isConstraintKind a && isConstraintKind b
+ = mkNthCo 0 $ constraintToLifted
+ $ mkSymCo $ constraintToLifted $ mkSymCo kind_co
+
+ | isConstraintKind a
+ = WARN( True, text "mkRuntimeRepCo" )
+ mkNthCo 0
+ $ mkSymCo $ constraintToLifted $ mkSymCo kind_co
+
+ | isConstraintKind b
+ = WARN( True, text "mkRuntimeRepCo" )
+ mkNthCo 0 $ constraintToLifted kind_co
+
+ | otherwise
+ = mkNthCo 0 kind_co
+ where
+ -- the right side of a coercion from Constraint to TYPE 'LiftedRep
+ constraintToLifted = (`mkTransCo` mkAxiomRuleCo constraintIsLifted [])
+
+ kind_co = mkKindCo co -- kind_co :: TYPE r1 ~ TYPE r2
+ -- (up to silliness with Constraint)
+ Pair a b = coercionKind kind_co -- Pair of (TYPE r1, TYPE r2)
+
-- | Tests if this coercion is obviously reflexive. Guaranteed to work
-- very quickly. Sometimes a coercion can be reflexive, but not obviously
-- so. c.f. 'isReflexiveCo'
@@ -538,8 +585,15 @@ mkNomReflCo = mkReflCo Nominal
-- | Apply a type constructor to a list of coercions. It is the
-- caller's responsibility to get the roles correct on argument coercions.
-mkTyConAppCo :: Role -> TyCon -> [Coercion] -> Coercion
+mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo r tc cos
+ | tc `hasKey` funTyConKey
+ , [_rep1, _rep2, co1, co2] <- cos
+ = -- (a :: TYPE ra) -> (b :: TYPE rb) ~ (c :: TYPE rc) -> (d :: TYPE rd)
+ -- rep1 :: ra ~ rc rep2 :: rb ~ rd
+ -- co1 :: a ~ c co2 :: b ~ d
+ mkFunCo r co1 co2
+
-- Expand type synonyms
| Just (tv_co_prs, rhs_ty, leftover_cos) <- expandSynTyCon_maybe tc cos
= mkAppCos (liftCoSubst r (mkLiftingContext tv_co_prs) rhs_ty) leftover_cos
@@ -549,9 +603,15 @@ mkTyConAppCo r tc cos
| otherwise = TyConAppCo r tc cos
--- | Make a function 'Coercion' between two other 'Coercion's
+-- | Build a function 'Coercion' from two other 'Coercion's. That is,
+-- given @co1 :: a ~ b@ and @co2 :: x ~ y@ produce @co :: (a -> x) ~ (b -> y)@.
mkFunCo :: Role -> Coercion -> Coercion -> Coercion
-mkFunCo r co1 co2 = mkTyConAppCo r funTyCon [co1, co2]
+mkFunCo r co1 co2
+ -- See Note [Refl invariant]
+ | Just (ty1, _) <- isReflCo_maybe co1
+ , Just (ty2, _) <- isReflCo_maybe co2
+ = Refl r (mkFunTy ty1 ty2)
+ | otherwise = FunCo r co1 co2
-- | Make nested function 'Coercion's
mkFunCos :: Role -> [Coercion] -> Coercion -> Coercion
@@ -569,7 +629,7 @@ mkAppCo (Refl r ty1) arg
| Just (tc, tys) <- splitTyConApp_maybe ty1
-- Expand type synonyms; a TyConAppCo can't have a type synonym (Trac #9102)
- = TyConAppCo r tc (zip_roles (tyConRolesX r tc) tys)
+ = mkTyConAppCo r tc (zip_roles (tyConRolesX r tc) tys)
where
zip_roles (r1:_) [] = [downgradeRole r1 Nominal arg]
zip_roles (r1:rs) (ty1:tys) = mkReflCo r1 ty1 : zip_roles rs tys
@@ -577,11 +637,11 @@ mkAppCo (Refl r ty1) arg
mkAppCo (TyConAppCo r tc args) arg
= case r of
- Nominal -> TyConAppCo Nominal tc (args ++ [arg])
- Representational -> TyConAppCo Representational tc (args ++ [arg'])
+ Nominal -> mkTyConAppCo Nominal tc (args ++ [arg])
+ Representational -> mkTyConAppCo Representational tc (args ++ [arg'])
where new_role = (tyConRolesRepresentational tc) !! (length args)
arg' = downgradeRole new_role Nominal arg
- Phantom -> TyConAppCo Phantom tc (args ++ [toPhantomCo arg])
+ Phantom -> mkTyConAppCo Phantom tc (args ++ [toPhantomCo arg])
mkAppCo co arg = AppCo co arg
-- Note, mkAppCo is careful to maintain invariants regarding
-- where Refl constructors appear; see the comments in the definition
@@ -839,7 +899,7 @@ mkNthCo 0 (Refl _ ty)
| Just (tv, _) <- splitForAllTy_maybe ty
= Refl Nominal (tyVarKind tv)
mkNthCo n (Refl r ty)
- = ASSERT( ok_tc_app ty n )
+ = ASSERT2( ok_tc_app ty n, ppr n $$ ppr ty )
mkReflCo r' (tyConAppArgN n ty)
where tc = tyConAppTyCon ty
r' = nthRole r tc n
@@ -857,6 +917,13 @@ mkNthCo 0 (ForAllCo _ kind_co _) = kind_co
-- If co :: (forall a1:k1. t1) ~ (forall a2:k2. t2)
-- then (nth 0 co :: k1 ~ k2)
mkNthCo n (TyConAppCo _ _ arg_cos) = arg_cos `getNth` n
+mkNthCo n co@(FunCo _ arg res)
+ = case n of
+ 0 -> mkRuntimeRepCo arg
+ 1 -> mkRuntimeRepCo res
+ 2 -> arg
+ 3 -> res
+ _ -> pprPanic "mkNthCo(FunCo)" (ppr n $$ ppr co)
mkNthCo n co = NthCo n co
mkLRCo :: LeftOrRight -> Coercion -> Coercion
@@ -894,6 +961,7 @@ infixl 5 `mkCoherenceCo`
infixl 5 `mkCoherenceRightCo`
infixl 5 `mkCoherenceLeftCo`
+-- | Given @co :: (a :: k) ~ (b :: k')@ produce @co' :: k ~ k'@.
mkKindCo :: Coercion -> Coercion
mkKindCo (Refl _ ty) = Refl Nominal (typeKind ty)
mkKindCo (UnivCo (PhantomProv h) _ _ _) = h
@@ -913,6 +981,10 @@ mkSubCo :: Coercion -> Coercion
mkSubCo (Refl Nominal ty) = Refl Representational ty
mkSubCo (TyConAppCo Nominal tc cos)
= TyConAppCo Representational tc (applyRoles tc cos)
+mkSubCo (FunCo Nominal arg res)
+ = FunCo Representational
+ (downgradeRole Representational Nominal arg)
+ (downgradeRole Representational Nominal res)
mkSubCo co = ASSERT2( coercionRole co == Nominal, ppr co <+> ppr (coercionRole co) )
SubCo co
@@ -980,6 +1052,11 @@ setNominalRole_maybe (Refl _ ty) = Just $ Refl Nominal ty
setNominalRole_maybe (TyConAppCo Representational tc cos)
= do { cos' <- mapM setNominalRole_maybe cos
; return $ TyConAppCo Nominal tc cos' }
+setNominalRole_maybe (FunCo Representational co1 co2)
+ = do { co1' <- setNominalRole_maybe co1
+ ; co2' <- setNominalRole_maybe co2
+ ; return $ FunCo Nominal co1' co2'
+ }
setNominalRole_maybe (SymCo co)
= SymCo <$> setNominalRole_maybe co
setNominalRole_maybe (TransCo co1 co2)
@@ -1088,6 +1165,9 @@ promoteCoercion co = case co of
ForAllCo _ _ g
-> promoteCoercion g
+ FunCo _ _ _
+ -> mkNomReflCo liftedTypeKind
+
CoVarCo {}
-> mkKindCo co
@@ -1167,7 +1247,7 @@ instCoercion (Pair lty rty) g w
, Just w' <- setNominalRole_maybe w
= Just $ mkInstCo g w'
| isFunTy lty && isFunTy rty
- = Just $ mkNthCo 1 g -- extract result type, which is the 2nd argument to (->)
+ = Just $ mkNthCo 3 g -- extract result type, which is the 4th argument to (->)
| otherwise -- one forall, one funty...
= Nothing
where
@@ -1195,6 +1275,8 @@ castCoercionKind g h1 h2
mkPiCos :: Role -> [Var] -> Coercion -> Coercion
mkPiCos r vs co = foldr (mkPiCo r) co vs
+-- | Make a forall 'Coercion', where both types related by the coercion
+-- are quantified over the same type variable.
mkPiCo :: Role -> Var -> Coercion -> Coercion
mkPiCo r v co | isTyVar v = mkHomoForAllCos [v] co
| otherwise = mkFunCo r (mkReflCo r (varType v)) co
@@ -1640,6 +1722,7 @@ seqCo (TyConAppCo r tc cos) = r `seq` tc `seq` seqCos cos
seqCo (AppCo co1 co2) = seqCo co1 `seq` seqCo co2
seqCo (ForAllCo tv k co) = seqType (tyVarKind tv) `seq` seqCo k
`seq` seqCo co
+seqCo (FunCo r co1 co2) = r `seq` seqCo co1 `seq` seqCo co2
seqCo (CoVarCo cv) = cv `seq` ()
seqCo (AxiomInstCo con ind cos) = con `seq` ind `seq` seqCos cos
seqCo (UnivCo p r t1 t2)
@@ -1714,6 +1797,7 @@ coercionKind co = go co
-- This is doing repeated substitutions and probably doesn't
-- need to, see #11735
mkInvForAllTy <$> Pair tv1 tv2 <*> Pair ty1 ty2'
+ go (FunCo _ co1 co2) = mkFunTy <$> go co1 <*> go co2
go (CoVarCo cv) = toPair $ coVarTypes cv
go (AxiomInstCo ax ind cos)
| CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
@@ -1794,6 +1878,8 @@ coercionKindRole = go
-- This is doing repeated substitutions and probably doesn't
-- need to, see #11735
(mkInvForAllTy <$> Pair tv1 tv2 <*> Pair ty1 ty2', r)
+ go (FunCo r co1 co2)
+ = (mkFunTy <$> coercionKind co1 <*> coercionKind co2, r)
go (CoVarCo cv) = (toPair $ coVarTypes cv, coVarRole cv)
go co@(AxiomInstCo ax _ _) = (coercionKind co, coAxiomRole ax)
go (UnivCo _ r ty1 ty2) = (Pair ty1 ty2, r)
@@ -1811,7 +1897,7 @@ coercionKindRole = go
= let (tc1, args1) = splitTyConApp ty1
(_tc2, args2) = splitTyConApp ty2
in
- ASSERT( tc1 == _tc2 )
+ ASSERT2( tc1 == _tc2, ppr d $$ ppr tc1 $$ ppr _tc2 )
((`getNth` d) <$> Pair args1 args2, nthRole r tc1 d)
where
diff --git a/compiler/types/Coercion.hs-boot b/compiler/types/Coercion.hs-boot
index 8ba92952b4..eefefd09e8 100644
--- a/compiler/types/Coercion.hs-boot
+++ b/compiler/types/Coercion.hs-boot
@@ -1,3 +1,5 @@
+{-# LANGUAGE FlexibleContexts #-}
+
module Coercion where
import {-# SOURCE #-} TyCoRep
@@ -8,11 +10,13 @@ import CoAxiom
import Var
import Outputable
import Pair
+import Util
mkReflCo :: Role -> Type -> Coercion
-mkTyConAppCo :: Role -> TyCon -> [Coercion] -> Coercion
+mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
mkAppCo :: Coercion -> Coercion -> Coercion
mkForAllCo :: TyVar -> Coercion -> Coercion -> Coercion
+mkFunCo :: Role -> Coercion -> Coercion -> Coercion
mkCoVarCo :: CoVar -> Coercion
mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
mkPhantomCo :: Coercion -> Type -> Type -> Coercion
diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs
index e605f7b4fd..89f4214766 100644
--- a/compiler/types/FamInstEnv.hs
+++ b/compiler/types/FamInstEnv.hs
@@ -1693,6 +1693,7 @@ allTyVarsInTy = go
go_co (AppCo co arg) = go_co co `unionVarSet` go_co arg
go_co (ForAllCo tv h co)
= unionVarSets [unitVarSet tv, go_co co, go_co h]
+ go_co (FunCo _ c1 c2) = go_co c1 `unionVarSet` go_co c2
go_co (CoVarCo cv) = unitVarSet cv
go_co (AxiomInstCo _ _ cos) = go_cos cos
go_co (UnivCo p _ t1 t2) = go_prov p `unionVarSet` go t1 `unionVarSet` go t2
diff --git a/compiler/types/OptCoercion.hs b/compiler/types/OptCoercion.hs
index 5e1f4547d9..5e4927fb70 100644
--- a/compiler/types/OptCoercion.hs
+++ b/compiler/types/OptCoercion.hs
@@ -207,6 +207,15 @@ opt_co4 env sym rep r (ForAllCo tv k_co co)
opt_co4_wrap env' sym rep r co
-- Use the "mk" functions to check for nested Refls
+opt_co4 env sym rep r (FunCo _r co1 co2)
+ = ASSERT( r == _r )
+ if rep
+ then mkFunCo Representational co1' co2'
+ else mkFunCo r co1' co2'
+ where
+ co1' = opt_co4_wrap env sym rep r co1
+ co2' = opt_co4_wrap env sym rep r co2
+
opt_co4 env sym rep r (CoVarCo cv)
| Just co <- lookupCoVar (lcTCvSubst env) cv
= opt_co4_wrap (zapLiftingContext env) sym rep r co
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index e4c1c979cb..1e90fa7aee 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -441,7 +441,8 @@ Pi-types:
* A non-dependent function type,
written with ->, e.g. ty1 -> ty2
- represented as FunTy ty1 ty2
+ represented as FunTy ty1 ty2. These are
+ lifted to Coercions with the corresponding FunCo.
* A dependent compile-time-only polytype,
written with forall, e.g. forall (a:*). ty
@@ -790,6 +791,9 @@ data Coercion
| ForAllCo TyVar KindCoercion Coercion
-- ForAllCo :: _ -> N -> e -> e
+ | FunCo Role Coercion Coercion -- lift FunTy
+ -- FunCo :: "e" -> e -> e -> e
+
-- These are special
| CoVarCo CoVar -- :: _ -> (N or R)
-- result role depends on the tycon of the variable's type
@@ -1440,6 +1444,8 @@ tyCoFVsOfCo (AppCo co arg) fv_cand in_scope acc
= (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc
tyCoFVsOfCo (ForAllCo tv kind_co co) fv_cand in_scope acc
= (delFV tv (tyCoFVsOfCo co) `unionFV` tyCoFVsOfCo kind_co) fv_cand in_scope acc
+tyCoFVsOfCo (FunCo _ co1 co2) fv_cand in_scope acc
+ = (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2) fv_cand in_scope acc
tyCoFVsOfCo (CoVarCo v) fv_cand in_scope acc
= (unitFV v `unionFV` tyCoFVsOfType (varType v)) fv_cand in_scope acc
tyCoFVsOfCo (AxiomInstCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc
@@ -1500,6 +1506,7 @@ coVarsOfCo (TyConAppCo _ _ args) = coVarsOfCos args
coVarsOfCo (AppCo co arg) = coVarsOfCo co `unionVarSet` coVarsOfCo arg
coVarsOfCo (ForAllCo tv kind_co co)
= coVarsOfCo co `delVarSet` tv `unionVarSet` coVarsOfCo kind_co
+coVarsOfCo (FunCo _ co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
coVarsOfCo (CoVarCo v) = unitVarSet v `unionVarSet` coVarsOfType (varType v)
coVarsOfCo (AxiomInstCo _ _ args) = coVarsOfCos args
coVarsOfCo (UnivCo p _ t1 t2) = coVarsOfProv p `unionVarSet` coVarsOfTypes [t1, t2]
@@ -1566,6 +1573,7 @@ noFreeVarsOfCo (Refl _ ty) = noFreeVarsOfType ty
noFreeVarsOfCo (TyConAppCo _ _ args) = all noFreeVarsOfCo args
noFreeVarsOfCo (AppCo c1 c2) = noFreeVarsOfCo c1 && noFreeVarsOfCo c2
noFreeVarsOfCo co@(ForAllCo {}) = isEmptyVarSet (tyCoVarsOfCo co)
+noFreeVarsOfCo (FunCo _ c1 c2) = noFreeVarsOfCo c1 && noFreeVarsOfCo c2
noFreeVarsOfCo (CoVarCo _) = False
noFreeVarsOfCo (AxiomInstCo _ _ args) = all noFreeVarsOfCo args
noFreeVarsOfCo (UnivCo p _ t1 t2) = noFreeVarsOfProv p &&
@@ -2234,6 +2242,7 @@ subst_co subst co
go (ForAllCo tv kind_co co)
= case substForAllCoBndrUnchecked subst tv kind_co of { (subst', tv', kind_co') ->
((mkForAllCo $! tv') $! kind_co') $! subst_co subst' co }
+ go (FunCo r co1 co2) = (mkFunCo r $! go co1) $! go co2
go (CoVarCo cv) = substCoVar subst cv
go (AxiomInstCo con ind cos) = mkAxiomInstCo con ind $! map go cos
go (UnivCo p r t1 t2) = (((mkUnivCo $! go_prov p) $! r) $!
@@ -2771,6 +2780,7 @@ tidyCo env@(_, subst) co
where (envp, tvp) = tidyTyCoVarBndr env tv
-- the case above duplicates a bit of work in tidying h and the kind
-- of tv. But the alternative is to use coercionKind, which seems worse.
+ go (FunCo r co1 co2) = (FunCo r $! go co1) $! go co2
go (CoVarCo cv) = case lookupVarEnv subst cv of
Nothing -> CoVarCo cv
Just cv' -> CoVarCo cv'
@@ -2833,6 +2843,7 @@ coercionSize (Refl _ ty) = typeSize ty
coercionSize (TyConAppCo _ _ args) = 1 + sum (map coercionSize args)
coercionSize (AppCo co arg) = coercionSize co + coercionSize arg
coercionSize (ForAllCo _ h co) = 1 + coercionSize co + coercionSize h
+coercionSize (FunCo _ co1 co2) = 1 + coercionSize co1 + coercionSize co2
coercionSize (CoVarCo _) = 1
coercionSize (AxiomInstCo _ _ args) = 1 + sum (map coercionSize args)
coercionSize (UnivCo p _ t1 t2) = 1 + provSize p + typeSize t1 + typeSize t2
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index 3aa2805616..1b80d20ad4 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -1391,7 +1391,7 @@ So we compromise, and move their Kind calculation to the call site.
-}
-- | Given the name of the function type constructor and it's kind, create the
--- corresponding 'TyCon'. It is reccomended to use 'TyCoRep.funTyCon' if you want
+-- corresponding 'TyCon'. It is recomended to use 'TyCoRep.funTyCon' if you want
-- this functionality
mkFunTyCon :: Name -> [TyConBinder] -> Name -> TyCon
mkFunTyCon name binders rep_nm
@@ -1401,7 +1401,7 @@ mkFunTyCon name binders rep_nm
tyConBinders = binders,
tyConResKind = liftedTypeKind,
tyConKind = mkTyConKind binders liftedTypeKind,
- tyConArity = 2,
+ tyConArity = length binders,
tcRepName = rep_nm
}
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 2cce7fe415..a50b76b2a3 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -47,6 +47,8 @@ module Type (
mkNumLitTy, isNumLitTy,
mkStrLitTy, isStrLitTy,
+ getRuntimeRep_maybe, getRuntimeRepFromKind_maybe,
+
mkCastTy, mkCoercionTy, splitCastTy_maybe,
userTypeError_maybe, pprUserTypeErrorTy,
@@ -385,6 +387,8 @@ expandTypeSynonyms ty
go_co subst (ForAllCo tv kind_co co)
= let (subst', tv', kind_co') = go_cobndr subst tv kind_co in
mkForAllCo tv' kind_co' (go_co subst' co)
+ go_co subst (FunCo r co1 co2)
+ = mkFunCo r (go_co subst co1) (go_co subst co2)
go_co subst (CoVarCo cv)
= substCoVar subst cv
go_co subst (AxiomInstCo ax ind args)
@@ -520,6 +524,7 @@ mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar
; co' <- mapCoercion mapper env' co
; return $ mkforallco tv' kind_co' co' }
-- See Note [Efficiency for mapCoercion ForAllCo case]
+ go (FunCo r c1 c2) = mkFunCo r <$> go c1 <*> go c2
go (CoVarCo cv) = covar env cv
go (AxiomInstCo ax i args)
= mkaxiominstco ax i <$> mapM go args
@@ -660,8 +665,15 @@ splitAppTy_maybe ty = repSplitAppTy_maybe ty
repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
-- ^ Does the AppTy split as in 'splitAppTy_maybe', but assumes that
-- any Core view stuff is already done
-repSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
-repSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
+repSplitAppTy_maybe (FunTy ty1 ty2)
+ | Just rep1 <- getRuntimeRep_maybe ty1
+ , Just rep2 <- getRuntimeRep_maybe ty2
+ = Just (TyConApp funTyCon [rep1, rep2, ty1], ty2)
+
+ | otherwise
+ = pprPanic "repSplitAppTy_maybe" (ppr ty1 $$ ppr ty2)
+repSplitAppTy_maybe (AppTy ty1 ty2)
+ = Just (ty1, ty2)
repSplitAppTy_maybe (TyConApp tc tys)
| mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
, Just (tys', ty') <- snocView tys
@@ -675,9 +687,16 @@ tcRepSplitAppTy_maybe :: Type -> Maybe (Type,Type)
-- ^ Does the AppTy split as in 'tcSplitAppTy_maybe', but assumes that
-- any coreView stuff is already done. Refuses to look through (c => t)
tcRepSplitAppTy_maybe (FunTy ty1 ty2)
- | isConstraintKind (typeKind ty1) = Nothing -- See Note [Decomposing fat arrow c=>t]
- | otherwise = Just (TyConApp funTyCon [ty1], ty2)
-tcRepSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
+ | isConstraintKind (typeKind ty1)
+ = Nothing -- See Note [Decomposing fat arrow c=>t]
+
+ | Just rep1 <- getRuntimeRep_maybe ty1
+ , Just rep2 <- getRuntimeRep_maybe ty2
+ = Just (TyConApp funTyCon [rep1, rep2, ty1], ty2)
+
+ | otherwise
+ = pprPanic "repSplitAppTy_maybe" (ppr ty1 $$ ppr ty2)
+tcRepSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
tcRepSplitAppTy_maybe (TyConApp tc tys)
| mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
, Just (tys', ty') <- snocView tys
@@ -707,9 +726,15 @@ splitAppTys ty = split ty ty []
(tc_args1, tc_args2) = splitAt n tc_args
in
(TyConApp tc tc_args1, tc_args2 ++ args)
- split _ (FunTy ty1 ty2) args = ASSERT( null args )
- (TyConApp funTyCon [], [ty1,ty2])
- split orig_ty _ args = (orig_ty, args)
+ split _ (FunTy ty1 ty2) args
+ | Just rep1 <- getRuntimeRep_maybe ty1
+ , Just rep2 <- getRuntimeRep_maybe ty2
+ = ASSERT( null args )
+ (TyConApp funTyCon [], [rep1, rep2, ty1, ty2])
+
+ | otherwise
+ = pprPanic "splitAppTys" (ppr ty1 $$ ppr ty2 $$ ppr args)
+ split orig_ty _ args = (orig_ty, args)
-- | Like 'splitAppTys', but doesn't look through type synonyms
repSplitAppTys :: Type -> (Type, [Type])
@@ -722,8 +747,14 @@ repSplitAppTys ty = split ty []
(tc_args1, tc_args2) = splitAt n tc_args
in
(TyConApp tc tc_args1, tc_args2 ++ args)
- split (FunTy ty1 ty2) args = ASSERT( null args )
- (TyConApp funTyCon [], [ty1, ty2])
+ split (FunTy ty1 ty2) args
+ | Just rep1 <- getRuntimeRep_maybe ty1
+ , Just rep2 <- getRuntimeRep_maybe ty2
+ = ASSERT( null args )
+ (TyConApp funTyCon [], [rep1, rep2, ty1, ty2])
+
+ | otherwise
+ = pprPanic "repSplitAppTys" (ppr ty1 $$ ppr ty2 $$ ppr args)
split ty args = (ty, args)
{-
@@ -795,6 +826,34 @@ pprUserTypeErrorTy ty =
---------------------------------------------------------------------
FunTy
~~~~~
+
+Note [Representation of function types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Functions (e.g. Int -> Char) are can be thought of as being applications
+of funTyCon (known in Haskell surface syntax as (->)),
+
+ (->) :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
+ (a :: TYPE r1) (b :: TYPE r2).
+ a -> b -> Type
+
+However, for efficiency's sake we represent saturated applications of (->)
+with FunTy. For instance, the type,
+
+ (->) r1 r2 a b
+
+is equivalent to,
+
+ FunTy (Anon a) b
+
+Note how the RuntimeReps are implied in the FunTy representation. For this
+reason we must be careful when recontructing the TyConApp representation (see,
+for instance, splitTyConApp_maybe).
+
+In the compiler we maintain the invariant that all saturated applications of
+(->) are represented with FunTy.
+
+See #11714.
-}
isFunTy :: Type -> Bool
@@ -937,7 +996,8 @@ applyTysX tvs body_ty arg_tys
-- its arguments. Applies its arguments to the constructor from left to right.
mkTyConApp :: TyCon -> [Type] -> Type
mkTyConApp tycon tys
- | isFunTyCon tycon, [ty1,ty2] <- tys
+ | isFunTyCon tycon
+ , [_rep1,_rep2,ty1,ty2] <- tys
= FunTy ty1 ty2
| otherwise
@@ -969,7 +1029,10 @@ tyConAppTyCon ty = tyConAppTyCon_maybe ty `orElse` pprPanic "tyConAppTyCon" (ppr
tyConAppArgs_maybe :: Type -> Maybe [Type]
tyConAppArgs_maybe ty | Just ty' <- coreView ty = tyConAppArgs_maybe ty'
tyConAppArgs_maybe (TyConApp _ tys) = Just tys
-tyConAppArgs_maybe (FunTy arg res) = Just [arg,res]
+tyConAppArgs_maybe (FunTy arg res)
+ | Just rep1 <- getRuntimeRep_maybe arg
+ , Just rep2 <- getRuntimeRep_maybe res
+ = Just [rep1, rep2, arg, res]
tyConAppArgs_maybe _ = Nothing
tyConAppArgs :: Type -> [Type]
@@ -992,16 +1055,22 @@ splitTyConApp ty = case splitTyConApp_maybe ty of
-- | Attempts to tease a type apart into a type constructor and the application
-- of a number of arguments to that constructor
-splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
+splitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
splitTyConApp_maybe ty = repSplitTyConApp_maybe ty
-- | Like 'splitTyConApp_maybe', but doesn't look through synonyms. This
-- assumes the synonyms have already been dealt with.
-repSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
+repSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
repSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
-repSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
-repSplitTyConApp_maybe _ = Nothing
+repSplitTyConApp_maybe (FunTy arg res)
+ | Just rep1 <- getRuntimeRep_maybe arg
+ , Just rep2 <- getRuntimeRep_maybe res
+ = Just (funTyCon, [rep1, rep2, arg, res])
+ | otherwise
+ = pprPanic "repSplitTyConApp_maybe"
+ (ppr arg $$ ppr res $$ ppr (typeKind res))
+repSplitTyConApp_maybe _ = Nothing
-- | Attempts to tease a list type apart and gives the type of the elements if
-- successful (looks through type synonyms)
@@ -1101,6 +1170,7 @@ mkCastTy ty co = -- NB: don't check if the coercion "from" type matches here;
ASSERT2( CastTy ty co `eqType` result
, ppr ty <+> dcolon <+> ppr (typeKind ty) $$
ppr co <+> dcolon <+> ppr (coercionKind co) $$
+ ppr (CastTy ty co) <+> dcolon <+> ppr (typeKind (CastTy ty co)) $$
ppr result <+> dcolon <+> ppr (typeKind result) )
result
where
@@ -1119,8 +1189,10 @@ mkCastTy ty co = -- NB: don't check if the coercion "from" type matches here;
saturated_tc (decomp_args `chkAppend` args) co
split_apps args (FunTy arg res) co
+ | rep_arg <- getRuntimeRep "mkCastTy.split_apps" arg
+ , rep_res <- getRuntimeRep "mkCastTy.split_apps" res
= affix_co (tyConTyBinders funTyCon) (mkTyConTy funTyCon)
- (arg : res : args) co
+ (rep_arg : rep_res : arg : res : args) co
split_apps args ty co
= affix_co (fst $ splitPiTys $ typeKind ty)
ty args co
@@ -1888,27 +1960,47 @@ isUnliftedType ty
= not (isLiftedType_maybe ty `orElse`
pprPanic "isUnliftedType" (ppr ty <+> dcolon <+> ppr (typeKind ty)))
--- | Extract the RuntimeRep classifier of a type. Panics if this is not possible.
+-- | Extract the RuntimeRep classifier of a type. For instance,
+-- @getRuntimeRep_maybe Int = LiftedRep@. Returns 'Nothing' if this is not
+-- possible.
+getRuntimeRep_maybe :: HasDebugCallStack
+ => Type -> Maybe Type
+getRuntimeRep_maybe = getRuntimeRepFromKind_maybe . typeKind
+
+-- | Extract the RuntimeRep classifier of a type. For instance,
+-- @getRuntimeRep_maybe Int = LiftedRep@. Panics if this is not possible.
getRuntimeRep :: HasDebugCallStack
=> String -- ^ Printed in case of an error
-> Type -> Type
-getRuntimeRep err ty = getRuntimeRepFromKind err (typeKind ty)
-
--- | Extract the RuntimeRep classifier of a type from its kind.
--- For example, getRuntimeRepFromKind * = LiftedRep;
--- Panics if this is not possible.
+getRuntimeRep err ty =
+ case getRuntimeRep_maybe ty of
+ Just r -> r
+ Nothing -> pprPanic "getRuntimeRep"
+ (text err $$ ppr ty <+> dcolon <+> ppr (typeKind ty))
+
+-- | Extract the RuntimeRep classifier of a type from its kind. For example,
+-- @getRuntimeRepFromKind * = LiftedRep@; Panics if this is not possible.
getRuntimeRepFromKind :: HasDebugCallStack
- => String -- ^ Printed in case of an error
- -> Type -> Type
-getRuntimeRepFromKind err = go
+ => String -> Type -> Type
+getRuntimeRepFromKind err k =
+ case getRuntimeRepFromKind_maybe k of
+ Just r -> r
+ Nothing -> pprPanic "getRuntimeRepFromKind"
+ (text err $$ ppr k <+> dcolon <+> ppr (typeKind k))
+
+-- | Extract the RuntimeRep classifier of a type from its kind. For example,
+-- @getRuntimeRepFromKind * = LiftedRep@; Returns 'Nothing' if this is not
+-- possible.
+getRuntimeRepFromKind_maybe :: HasDebugCallStack
+ => Type -> Maybe Type
+getRuntimeRepFromKind_maybe = go
where
go k | Just k' <- coreViewOneStarKind k = go k'
go k
- | (_tc, [arg]) <- splitTyConApp k
- = ASSERT2( _tc `hasKey` tYPETyConKey, text err $$ ppr k )
- arg
- go k = pprPanic "getRuntimeRep" (text err $$
- ppr k <+> dcolon <+> ppr (typeKind k))
+ | Just (_tc, [arg]) <- splitTyConApp_maybe k
+ = ASSERT2( _tc `hasKey` tYPETyConKey, ppr k )
+ Just arg
+ go _ = Nothing
isUnboxedTupleType :: Type -> Bool
isUnboxedTupleType ty
@@ -2170,6 +2262,7 @@ nonDetCmpTypeX env orig_t1 orig_t2 =
go _ (LitTy l1) (LitTy l2) = liftOrdering (compare l1 l2)
go env (CastTy t1 _) t2 = hasCast $ go env t1 t2
go env t1 (CastTy t2 _) = hasCast $ go env t1 t2
+
go _ (CoercionTy {}) (CoercionTy {}) = TEQ
-- Deal with the rest: TyVarTy < CoercionTy < AppTy < LitTy < TyConApp < ForAllTy
@@ -2291,6 +2384,7 @@ tyConsOfType ty
go_co (TyConAppCo _ tc args) = go_tc tc `plusNameEnv` go_cos args
go_co (AppCo co arg) = go_co co `plusNameEnv` go_co arg
go_co (ForAllCo _ kind_co co) = go_co kind_co `plusNameEnv` go_co co
+ go_co (FunCo _ co1 co2) = go_co co1 `plusNameEnv` go_co co2
go_co (CoVarCo {}) = emptyNameEnv
go_co (AxiomInstCo ax _ args) = go_ax ax `plusNameEnv` go_cos args
go_co (UnivCo p _ t1 t2) = go_prov p `plusNameEnv` go t1 `plusNameEnv` go t2
diff --git a/compiler/types/Unify.hs b/compiler/types/Unify.hs
index 0ee895a4ba..41b8c6138d 100644
--- a/compiler/types/Unify.hs
+++ b/compiler/types/Unify.hs
@@ -1162,8 +1162,8 @@ data MatchEnv = ME { me_tmpls :: TyVarSet
, me_env :: RnEnv2 }
-- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'. In particular, if
--- @liftCoMatch vars ty co == Just s@, then @tyCoSubst s ty == co@,
--- where @==@ there means that the result of tyCoSubst has the same
+-- @liftCoMatch vars ty co == Just s@, then @listCoSubst s ty == co@,
+-- where @==@ there means that the result of 'liftCoSubst' has the same
-- type as the original co; but may be different under the hood.
-- That is, it matches a type against a coercion of the same
-- "shape", and returns a lifting substitution which could have been
@@ -1269,8 +1269,15 @@ ty_co_match menv subst ty1 (AppCo co2 arg2) _lkco _rkco
ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo _ tc2 cos) _lkco _rkco
= ty_co_match_tc menv subst tc1 tys tc2 cos
-ty_co_match menv subst (FunTy ty1 ty2) (TyConAppCo _ tc cos) _lkco _rkco
- = ty_co_match_tc menv subst funTyCon [ty1, ty2] tc cos
+ty_co_match menv subst (FunTy ty1 ty2) co _lkco _rkco
+ -- Despite the fact that (->) is polymorphic in four type variables (two
+ -- runtime rep and two types), we shouldn't need to explicitly unify the
+ -- runtime reps here; unifying the types themselves should be sufficient.
+ -- See Note [Representation of function types].
+ | Just (tc, [_,_,co1,co2]) <- splitTyConAppCo_maybe co
+ , tc == funTyCon
+ = let Pair lkcos rkcos = traverse (fmap mkNomReflCo . coercionKind) [co1,co2]
+ in ty_co_match_args menv subst [ty1, ty2] [co1, co2] lkcos rkcos
ty_co_match menv subst (ForAllTy (TvBndr tv1 _) ty1)
(ForAllCo tv2 kind_co2 co2)
@@ -1334,7 +1341,10 @@ pushRefl :: Coercion -> Maybe Coercion
pushRefl (Refl Nominal (AppTy ty1 ty2))
= Just (AppCo (Refl Nominal ty1) (mkNomReflCo ty2))
pushRefl (Refl r (FunTy ty1 ty2))
- = Just (TyConAppCo r funTyCon [mkReflCo r ty1, mkReflCo r ty2])
+ | Just rep1 <- getRuntimeRep_maybe ty1
+ , Just rep2 <- getRuntimeRep_maybe ty2
+ = Just (TyConAppCo r funTyCon [ mkReflCo r rep1, mkReflCo r rep2
+ , mkReflCo r ty1, mkReflCo r ty2 ])
pushRefl (Refl r (TyConApp tc tys))
= Just (TyConAppCo r tc (zipWith mkReflCo (tyConRolesX r tc) tys))
pushRefl (Refl r (ForAllTy (TvBndr tv _) ty))
View Lorry Controller Status