-{- 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')
- expand (TransCoercion t1 t2) = do
- exp1 <- expand t1
- exp2 <- expand t2
- return $ TransCoercion exp1 exp2
- expand (SymCoercion t) = do
- exp <- expand t
- return $ SymCoercion exp
- expand (UnsafeCoercion t1 t2) = do
- exp1 <- expand t1
- exp2 <- expand t2
- return $ UnsafeCoercion exp1 exp2
- expand (LeftCoercion t1) = do
- exp1 <- expand t1
- return $ LeftCoercion exp1
- expand (RightCoercion t1) = do
- exp1 <- expand t1
- return $ RightCoercion exp1
- expand (InstCoercion t1 t2) = do
- exp1 <- expand t1
- exp2 <- expand t2
- return $ InstCoercion exp1 exp2
- 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)
-