%
\begin{code}
-{-# OPTIONS -w #-}
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and fix
-- any warnings in the module. See
co_con_arity = length tvs
rule :: CoTyConKindChecker
- rule kc_ty kc_co checking args
+ rule kc_ty _kc_co checking args
= do { ks <- mapM kc_ty args
; unless (not checking || kindAppOk (tyConKind tycon) ks)
(fail "Argument kind mis-match")
coArity = length tvs
rule :: CoTyConKindChecker
- rule kc_ty kc_co checking args
+ rule kc_ty _kc_co checking args
= do { ks <- mapM kc_ty args
; unless (not checking || kindAppOk (tyConKind rep_tycon) ks)
(fail "Argument kind mis-match")
, TyConApp rep_tycon args) } -- ~ R tys
kindAppOk :: Kind -> [Kind] -> Bool
-kindAppOk kfn [] = True
+kindAppOk _ [] = True
kindAppOk kfn (k:ks)
= case splitKindFunTy_maybe kfn of
Just (kfa, kfb) | k `isSubKind` kfa -> kindAppOk kfb ks
= mkCoercionTyCon symCoercionTyConName 1 kc_sym
where
kc_sym :: CoTyConKindChecker
- kc_sym kc_ty kc_co _ (co:_)
+ kc_sym _kc_ty kc_co _ (co:_)
= do { (ty1,ty2) <- kc_co co
; return (ty2,ty1) }
+ kc_sym _ _ _ _ = panic "kc_sym"
transCoercionTyCon
= mkCoercionTyCon transCoercionTyConName 2 kc_trans
where
kc_trans :: CoTyConKindChecker
- kc_trans kc_ty kc_co checking (co1:co2:_)
+ kc_trans _kc_ty kc_co checking (co1:co2:_)
= do { (a1, r1) <- kc_co co1
; (a2, r2) <- kc_co co2
; unless (not checking || (r1 `coreEqType` a2))
(fail "Trans coercion mis-match")
; return (a1, r2) }
+ kc_trans _ _ _ _ = panic "kc_sym"
---------------------------------------------------
leftCoercionTyCon = mkCoercionTyCon leftCoercionTyConName 1 (kcLR_help fst)
rightCoercionTyCon = mkCoercionTyCon rightCoercionTyConName 1 (kcLR_help snd)
kcLR_help :: (forall a. (a,a)->a) -> CoTyConKindChecker
-kcLR_help select kc_ty kc_co _checking (co : _)
+kcLR_help select _kc_ty kc_co _checking (co : _)
= do { (ty1, ty2) <- kc_co co
; case decompLR_maybe ty1 ty2 of
Nothing -> fail "decompLR"
Just res -> return (select res) }
+kcLR_help _ _ _ _ _ = panic "kcLR_help"
decompLR_maybe :: Type -> Type -> Maybe ((Type,Type), (Type,Type))
-- Helper for left and right. Finds coercion kind of its input and
(fail "Coercion instantation kind mis-match")
; return (substTyWith [tv1] [ty] ty1,
substTyWith [tv2] [ty] ty2) } }
+ kcInst_help _ _ _ _ = panic "kcInst_help"
decompInst_maybe :: Type -> Type -> Maybe ((TyVar,TyVar), (Type,Type))
decompInst_maybe ty1 ty2
| Just (tv1,r1) <- splitForAllTy_maybe ty1
, Just (tv2,r2) <- splitForAllTy_maybe ty2
= Just ((tv1,tv2), (r1,r2))
-
+decompInst_maybe _ _ = Nothing
---------------------------------------------------
unsafeCoercionTyCon
= mkCoercionTyCon unsafeCoercionTyConName 2 kc_unsafe
where
- kc_unsafe kc_ty kc_co _checking (ty1:ty2:_)
- = do { k1 <- kc_ty ty1
- ; k2 <- kc_ty ty2
+ kc_unsafe kc_ty _kc_co _checking (ty1:ty2:_)
+ = do { _ <- kc_ty ty1
+ ; _ <- kc_ty ty2
; return (ty1,ty2) }
+ kc_unsafe _ _ _ _ = panic "kc_unsafe"
---------------------------------------------------
-- The csel* family
cselRCoercionTyCon = mkCoercionTyCon cselRCoercionTyConName 1 (kcCsel_help thirdOf3)
kcCsel_help :: (forall a. (a,a,a) -> a) -> CoTyConKindChecker
-kcCsel_help select kc_ty kc_co _checking (co : rest)
+kcCsel_help select _kc_ty kc_co _checking (co : _)
= do { (ty1,ty2) <- kc_co co
; case decompCsel_maybe ty1 ty2 of
Nothing -> fail "decompCsel"
Just res -> return (select res) }
+kcCsel_help _ _ _ _ _ = panic "kcCsel_help"
decompCsel_maybe :: Type -> Type -> Maybe ((Type,Type), (Type,Type), (Type,Type))
-- If co :: (s1~t1 => r1) ~ (s2~t2 => r2)
-- | Extract a 'Coercion' from a 'CoercionI' if it represents one. If it is the identity coercion,
-- panic
fromACo :: CoercionI -> Coercion
-fromACo (ACo co) = co
+fromACo (ACo co) = co
+fromACo (IdCo {}) = panic "fromACo"
-- | Smart constructor for class 'Coercion's on 'CoercionI'. Satisfies:
--
%************************************************************************
\begin{code}
+optCoercion :: TvSubst -> Coercion -> NormalCo
+-- ^ optCoercion applies a substitution to a coercion,
+-- *and* optimises it to reduce its size
+optCoercion env co = opt_co env False co
+
type NormalCo = Coercion
-- Invariants:
+ -- * The substitution has been fully applied
-- * For trans coercions (co1 `trans` co2)
-- co1 is not a trans, and neither co1 nor co2 is identity
-- * If the coercion is the identity, it has no CoVars of CoTyCons in it (just types)
type NormalNonIdCo = NormalCo -- Extra invariant: not the identity
-optCoercion :: Coercion -> NormalCo
-optCoercion co = opt_co False co
-
-opt_co :: Bool -- True <=> return (sym co)
- -> Coercion
- -> NormalCo
+opt_co, opt_co' :: TvSubst
+ -> Bool -- True <=> return (sym co)
+ -> Coercion
+ -> NormalCo
opt_co = opt_co'
-- opt_co sym co = pprTrace "opt_co {" (ppr sym <+> ppr co) $
-- co1 `seq`
-- | otherwise = (s,t)
-- (s2,t2) = coercionKind co1
-opt_co' sym (AppTy ty1 ty2) = mkAppTy (opt_co sym ty1) (opt_co sym ty2)
-opt_co' sym (FunTy ty1 ty2) = FunTy (opt_co sym ty1) (opt_co sym ty2)
-opt_co' sym (PredTy (ClassP cls tys)) = PredTy (ClassP cls (map (opt_co sym) tys))
-opt_co' sym (PredTy (IParam n ty)) = PredTy (IParam n (opt_co sym ty))
+opt_co' env sym (AppTy ty1 ty2) = mkAppTy (opt_co env sym ty1) (opt_co env sym ty2)
+opt_co' env sym (FunTy ty1 ty2) = FunTy (opt_co env sym ty1) (opt_co env sym ty2)
+opt_co' env sym (PredTy (ClassP cls tys)) = PredTy (ClassP cls (map (opt_co env sym) tys))
+opt_co' env sym (PredTy (IParam n ty)) = PredTy (IParam n (opt_co env sym ty))
+opt_co' _ _ co@(PredTy (EqPred {})) = pprPanic "optCoercion" (ppr co)
-opt_co' sym co@(TyVarTy tv)
+opt_co' env sym co@(TyVarTy tv)
+ | Just ty <- lookupTyVar env tv = opt_co' (zapTvSubstEnv env) sym ty
| not (isCoVar tv) = co -- Identity; does not mention a CoVar
| ty1 `coreEqType` ty2 = ty1 -- Identity; ..ditto..
| not sym = co
where
(ty1,ty2) = coVarKind tv
-opt_co' sym (ForAllTy tv cor)
- | isCoVar tv = mkCoPredTy (opt_co sym co1) (opt_co sym co2) (opt_co sym cor)
- | otherwise = ForAllTy tv (opt_co sym cor)
+opt_co' env sym (ForAllTy tv cor)
+ | isCoVar tv = mkCoPredTy (opt_co env sym co1) (opt_co env sym co2) (opt_co env sym cor)
+ | otherwise = case substTyVarBndr env tv of
+ (env', tv') -> ForAllTy tv' (opt_co env' sym cor)
where
(co1,co2) = coVarKind tv
-opt_co' sym (TyConApp tc cos)
+opt_co' env sym (TyConApp tc cos)
| isCoercionTyCon tc
- = foldl mkAppTy opt_co_tc
- (map (opt_co sym) (drop arity cos))
+ = foldl mkAppTy
+ (opt_co_tc_app env sym tc (take arity cos))
+ (map (opt_co env sym) (drop arity cos))
| otherwise
- = TyConApp tc (map (opt_co sym) cos)
+ = TyConApp tc (map (opt_co env sym) cos)
where
arity = tyConArity tc
- opt_co_tc :: NormalCo
- opt_co_tc = opt_co_tc_app sym tc (take arity cos)
--------
-opt_co_tc_app :: Bool -> TyCon -> [Type] -> NormalCo
+opt_co_tc_app :: TvSubst -> Bool -> TyCon -> [Coercion] -> NormalCo
-- Used for CoercionTyCons only
-opt_co_tc_app sym tc cos
+-- Arguments are *not* already simplified/substituted
+opt_co_tc_app env sym tc cos
| tc `hasKey` symCoercionTyConKey
- = opt_co (not sym) co1
+ = opt_co env (not sym) co1
| tc `hasKey` transCoercionTyConKey
- = if sym then opt_trans opt_co2 opt_co1
+ = if sym then opt_trans opt_co2 opt_co1 -- sym (g `o` h) = sym h `o` sym g
else opt_trans opt_co1 opt_co2
| tc `hasKey` leftCoercionTyConKey
- , Just (co1, _) <- splitAppTy_maybe opt_co1
- = co1
+ , Just (opt_co1_left, _) <- splitAppTy_maybe opt_co1
+ = opt_co1_left -- sym (left g) = left (sym g)
+ -- The opt_co has the sym pushed into it
| tc `hasKey` rightCoercionTyConKey
- , Just (_, co2) <- splitAppTy_maybe opt_co1
- = co2
+ , Just (_, opt_co1_right) <- splitAppTy_maybe opt_co1
+ = opt_co1_right
| tc `hasKey` csel1CoercionTyConKey
, Just (s1,_,_) <- splitCoPredTy_maybe opt_co1
, Just (_,_,r) <- splitCoPredTy_maybe opt_co1
= r
- | tc `hasKey` instCoercionTyConKey
- , Just (tv, co'') <- splitForAllTy_maybe opt_co1
- , let ty = co2
- = substTyWith [tv] [ty] co''
+ | tc `hasKey` instCoercionTyConKey -- See if the first arg
+ -- is already a forall
+ , Just (tv, co1_body) <- splitForAllTy_maybe co1
+ , let ty = substTy env co2
+ = opt_co (extendTvSubst env tv ty) sym co1_body
- | otherwise -- Do not push sym inside top-level axioms
+ | tc `hasKey` instCoercionTyConKey -- See if is *now* a forall
+ , Just (tv, opt_co1_body) <- splitForAllTy_maybe opt_co1
+ , let ty = substTy env co2
+ = substTyWith [tv] [ty] opt_co1_body -- An inefficient one-variable substitution
+
+ | otherwise -- Do *not* push sym inside top-level axioms
-- e.g. if g is a top-level axiom
-- g a : F a ~ a
-- Then (sym (g ty)) /= g (sym ty) !!
= if sym then mkSymCoercion the_co
else the_co
where
- the_co = TyConApp tc cos
(co1 : cos1) = cos
(co2 : _) = cos1
- opt_co1 = opt_co sym co1
- opt_co2 = opt_co sym co2
+
+ -- These opt_cos have the sym pushed into them
+ opt_co1 = opt_co env sym co1
+ opt_co2 = opt_co env sym co2
+
+ -- However the_co does *not* have sym pushed into it
+ the_co = TyConApp tc (map (opt_co env False) cos)
-------------
opt_trans :: NormalCo -> NormalCo -> NormalCo
projects / ghc-hetmet.git / blobdiff