Commit b207b536 authored by Ben Gamari's avatar Ben Gamari 🐢

Generalize kind of the (->) tycon

This is generalizes the kind of `(->)`, as discussed in #11714.

This involves a few things,

 * Generalizing the kind of `funTyCon`, adding two new `RuntimeRep`
binders,
  ```lang=haskell
(->) :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
               (a :: TYPE r1) (b :: TYPE r2).
        a -> b -> *
  ```

 * Unsaturated applications of `(->)` are expressed as explicit
`TyConApp`s

 * Saturated applications of `(->)` are expressed as `FunTy` as they are
currently

 * Saturated applications of `(->)` are expressed by a new `FunCo`
constructor in coercions

 * `splitTyConApp` needs to ensure that `FunTy`s are split to a
`TyConApp`
   of `(->)` with the appropriate `RuntimeRep` arguments

 * Teach CoreLint to check that all saturated applications of `(->)` are
represented with `FunTy`

At the moment I assume that `Constraint ~ *`, which is an annoying
source of complexity. This will
be simplified once D3023 is resolved.

Also, this introduces two known regressions,

`tcfail181`, `T10403`
=====================
Only shows the instance,

    instance Monad ((->) r) -- Defined in ‘GHC.Base’

in its error message when -fprint-potential-instances is used. This is
because its instance head now mentions 'LiftedRep which is not in scope.
I'm not entirely sure of the right way to fix this so I'm just accepting
the new output for now.

T5963 (Typeable)
================

T5963 is now broken since Data.Typeable.Internals.mkFunTy computes its
fingerprint without the RuntimeRep variables that (->) expects. This
will be fixed with the merge of D2010.

Haddock performance
===================

The `haddock.base` and `haddock.Cabal` tests regress in allocations by
about 20%. This certainly hurts, but it's also not entirely unexpected:
the size of every function type grows with this patch and Haddock has a
lot of functions in its heap.
parent efeaf9e4
......@@ -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
......
......@@ -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)
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
{-
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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'
......
......@@ -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.
......
......@@ -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
......
......@@ -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
......
......@@ -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