+ do tvenv' <- extendTvenv tvenv tb
+ checkTy (tcenv,tvenv') t
+ ch (TransCoercion t1 t2) = do
+ (ty1,ty2) <- checkTyCo es t1
+ (ty3,ty4) <- checkTyCo es t2
+ require (ty2 == ty3) ("Types don't match in trans. coercion: " ++
+ show ty2 ++ " and " ++ show ty3)
+ return $ Keq ty1 ty4
+ ch (SymCoercion t1) = do
+ (ty1,ty2) <- checkTyCo es t1
+ return $ Keq ty2 ty1
+ ch (UnsafeCoercion t1 t2) = do
+ checkTy es t1
+ checkTy es t2
+ return $ Keq t1 t2
+ ch (LeftCoercion t1) = do
+ k <- checkTyCo es t1
+ case k of
+ ((Tapp u _), (Tapp w _)) -> return $ Keq u w
+ _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
+ ch (RightCoercion t1) = do
+ k <- checkTyCo es t1
+ case k of
+ ((Tapp _ v), (Tapp _ x)) -> return $ Keq v x
+ _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
+ ch (InstCoercion ty arg) = do
+ forallK <- checkTyCo es ty
+ case forallK of
+ ((Tforall (v1,k1) b1), (Tforall (v2,k2) b2)) -> do
+ require (k1 `eqKind` k2) ("Kind mismatch in argument of inst: "
+ ++ show ty)
+ argK <- checkTy es arg
+ require (argK `eqKind` k1) ("Kind mismatch in type being "
+ ++ "instantiated: " ++ show arg)
+ let newLhs = substl [v1] [arg] b1
+ let newRhs = substl [v2] [arg] b2
+ return $ Keq newLhs newRhs
+ _ -> fail ("Non-forall-ty in argument to inst: " ++ show ty)
+
+checkTyCo :: (Tcenv, Tvenv) -> Ty -> CheckResult (Ty, Ty)
+checkTyCo es@(tcenv,_) t@(Tapp t1 t2) =
+ (case splitTyConApp_maybe t of
+ Just (tc, tys) -> do
+ tcK <- qlookupM tcenv_ tcenv eempty tc
+ case tcK of
+ -- todo: avoid duplicating this code
+ -- blah, this almost calls for a different syntactic form
+ -- (for a defined-coercion app): (TCoercionApp Tcon [Ty])
+ Coercion (DefinedCoercion tbs (from, to)) -> do
+ require (length tys == length tbs) $
+ ("Arity mismatch in coercion app: " ++ show t)
+ let (tvs, tks) = unzip tbs
+ argKs <- mapM (checkTy es) tys
+ let kPairs = zip argKs tks
+ let kindsOk = all (uncurry eqKind) kPairs
+ if not kindsOk &&
+ all (uncurry subKindOf) kPairs
+ -- see comments in checkTy about this
+ then warn $ "Applying coercion " ++ show tc ++
+ " to arguments of kind " ++ show argKs
+ ++ " when it expects: " ++ show tks
+ else require kindsOk
+ ("Kind mismatch in coercion app: " ++ show tks
+ ++ " and " ++ show argKs ++ " t = " ++ show t)
+ return (substl tvs tys from, substl tvs tys to)
+ _ -> checkTapp t1 t2
+ _ -> checkTapp t1 t2)
+ where checkTapp t1 t2 = do
+ (lhsRator, rhsRator) <- checkTyCo es t1
+ (lhs, rhs) <- checkTyCo es t2
+ -- Comp rule from paper
+ checkTy es (Tapp lhsRator lhs)
+ checkTy es (Tapp rhsRator rhs)
+ return (Tapp lhsRator lhs, Tapp rhsRator rhs)
+checkTyCo (tcenv, tvenv) (Tforall tb t) = do
+ tvenv' <- extendTvenv tvenv tb
+ (t1,t2) <- checkTyCo (tcenv, tvenv') t
+ return (Tforall tb t1, Tforall tb t2)
+checkTyCo es t = do
+ k <- checkTy es t
+ case k of
+ Keq t1 t2 -> return (t1, t2)
+ -- otherwise, expand by the "refl" rule
+ _ -> return (t, t)
+
projects / ghc-hetmet.git / blobdiff