- do tvenv' <- extendM tvenv tb
- checkTy (tcenv,tvenv') t
-
-{- Type equality modulo newtype synonyms. -}
-equalTy :: Tsenv -> Ty -> Ty -> CheckResult Bool
-equalTy tsenv t1 t2 =
- do t1' <- expand t1
- t2' <- expand t2
- return (t1' == t2')
- where expand (Tvar v) = return (Tvar v)
- expand (Tcon qtc) = return (Tcon qtc)
- expand (Tapp t1 t2) =
- do t2' <- expand t2
- expapp t1 [t2']
- expand (Tforall tb t) =
- do t' <- expand t
- return (Tforall tb t')
- expapp (t@(Tcon (m,tc))) ts =
- do env <- mlookupM tsenv_ tsenv eempty m
- case elookup env tc of
- Just (formals,rhs) | (length formals) == (length ts) -> return (substl formals ts rhs)
- _ -> return (foldl Tapp t ts)
- expapp (Tapp t1 t2) ts =
- do t2' <- expand t2
- expapp t1 (t2':ts)
- expapp t ts =
- do t' <- expand t
- return (foldl Tapp t' ts)
-
+ 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 subKindOf) kPairs
+ 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)