module Language.PureScript.TypeChecker.Types (
typesOf
) where
import Data.List
import Data.Maybe (maybeToList, fromMaybe)
import Data.Function (on)
import Data.Ord (comparing)
import Data.Monoid
import Data.Either (lefts, rights)
import Language.PureScript.Declarations
import Language.PureScript.Types
import Language.PureScript.Kinds
import Language.PureScript.Names
import Language.PureScript.TypeClassDictionaries
import Language.PureScript.TypeChecker.Monad
import Language.PureScript.TypeChecker.Kinds
import Language.PureScript.TypeChecker.Synonyms
import Language.PureScript.Pretty
import Language.PureScript.Environment
import Language.PureScript.Errors
import qualified Language.PureScript.Constants as C
import Control.Monad.State
import Control.Monad.Error
import Control.Monad.Unify
import Control.Applicative
import Control.Arrow (Arrow(..))
import qualified Data.Map as M
import qualified Data.HashMap.Strict as H
instance Partial Type where
unknown = TUnknown
isUnknown (TUnknown u) = Just u
isUnknown _ = Nothing
unknowns = everythingOnTypes (++) go
where
go (TUnknown u) = [u]
go _ = []
($?) sub = everywhereOnTypes go
where
go t@(TUnknown u) = case H.lookup u (runSubstitution sub) of
Nothing -> t
Just t' -> t'
go other = other
instance Unifiable Check Type where
(=?=) = unifyTypes
unifyTypes :: Type -> Type -> UnifyT Type Check ()
unifyTypes t1 t2 = rethrow (mkErrorStack ("Error unifying type " ++ prettyPrintType t1 ++ " with type " ++ prettyPrintType t2) Nothing <>) $
unifyTypes' t1 t2
where
unifyTypes' (TUnknown u1) (TUnknown u2) | u1 == u2 = return ()
unifyTypes' (TUnknown u) t = u =:= t
unifyTypes' t (TUnknown u) = u =:= t
unifyTypes' (SaturatedTypeSynonym name args) ty = do
ty1 <- introduceSkolemScope <=< expandTypeSynonym name $ args
ty1 `unifyTypes` ty
unifyTypes' ty s@(SaturatedTypeSynonym _ _) = s `unifyTypes` ty
unifyTypes' (ForAll ident1 ty1 sc1) (ForAll ident2 ty2 sc2) =
case (sc1, sc2) of
(Just sc1', Just sc2') -> do
sko <- newSkolemConstant
let sk1 = skolemize ident1 sko sc1' ty1
let sk2 = skolemize ident2 sko sc2' ty2
sk1 `unifyTypes` sk2
_ -> error "Skolemized type variable was not given a scope"
unifyTypes' (ForAll ident ty1 (Just sc)) ty2 = do
sko <- newSkolemConstant
let sk = skolemize ident sko sc ty1
sk `unifyTypes` ty2
unifyTypes' ForAll{} _ = throwError . strMsg $ "Skolem variable scope is unspecified"
unifyTypes' ty f@ForAll{} = f `unifyTypes` ty
unifyTypes' (TypeVar v1) (TypeVar v2) | v1 == v2 = return ()
unifyTypes' (TypeConstructor c1) (TypeConstructor c2) =
guardWith (strMsg ("Cannot unify " ++ show c1 ++ " with " ++ show c2 ++ ".")) (c1 == c2)
unifyTypes' (TypeApp t3 t4) (TypeApp t5 t6) = do
t3 `unifyTypes` t5
t4 `unifyTypes` t6
unifyTypes' (Skolem _ s1 _) (Skolem _ s2 _) | s1 == s2 = return ()
unifyTypes' (KindedType ty1 _) ty2 = ty1 `unifyTypes` ty2
unifyTypes' ty1 (KindedType ty2 _) = ty1 `unifyTypes` ty2
unifyTypes' r1@RCons{} r2 = unifyRows r1 r2
unifyTypes' r1 r2@RCons{} = unifyRows r1 r2
unifyTypes' r1@REmpty r2 = unifyRows r1 r2
unifyTypes' r1 r2@REmpty = unifyRows r1 r2
unifyTypes' t@(ConstrainedType _ _) _ = throwError . strMsg $ "Attempted to unify a constrained type " ++ prettyPrintType t ++ " with another type."
unifyTypes' t3 t4@(ConstrainedType _ _) = unifyTypes' t4 t3
unifyTypes' t3 t4 = throwError . strMsg $ "Cannot unify " ++ prettyPrintType t3 ++ " with " ++ prettyPrintType t4 ++ "."
unifyRows :: Type -> Type -> UnifyT Type Check ()
unifyRows r1 r2 =
let
(s1, r1') = rowToList r1
(s2, r2') = rowToList r2
int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
in do
forM_ int (uncurry (=?=))
unifyRows' sd1 r1' sd2 r2'
where
unifyRows' :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> UnifyT Type Check ()
unifyRows' [] (TUnknown u) sd r = u =:= rowFromList (sd, r)
unifyRows' sd r [] (TUnknown u) = u =:= rowFromList (sd, r)
unifyRows' sd1 (TUnknown u1) sd2 (TUnknown u2) = do
forM_ sd1 $ \(_, t) -> occursCheck u2 t
forM_ sd2 $ \(_, t) -> occursCheck u1 t
rest <- fresh
u1 =:= rowFromList (sd2, rest)
u2 =:= rowFromList (sd1, rest)
unifyRows' [] REmpty [] REmpty = return ()
unifyRows' [] (TypeVar v1) [] (TypeVar v2) | v1 == v2 = return ()
unifyRows' [] (Skolem _ s1 _) [] (Skolem _ s2 _) | s1 == s2 = return ()
unifyRows' sd3 r3 sd4 r4 = throwError . strMsg $ "Cannot unify (" ++ prettyPrintRow (rowFromList (sd3, r3)) ++ ") with (" ++ prettyPrintRow (rowFromList (sd4, r4)) ++ ")"
typesOf :: Maybe ModuleName -> ModuleName -> [(Ident, Expr)] -> Check [(Ident, (Expr, Type))]
typesOf mainModuleName moduleName vals = do
tys <- fmap tidyUp . liftUnify $ do
(untyped, typed, dict, untypedDict) <- typeDictionaryForBindingGroup moduleName vals
ds1 <- parU typed $ \e -> do
triple@(_, (_, ty)) <- checkTypedBindingGroupElement moduleName e dict
checkMain (fst e) ty
return triple
ds2 <- forM untyped $ \e -> do
triple@(_, (_, ty)) <- typeForBindingGroupElement e dict untypedDict
checkMain (fst e) ty
return triple
return $ ds1 ++ ds2
forM tys $ \(ident, (val, ty)) -> do
val' <- replaceTypeClassDictionaries moduleName val
skolemEscapeCheck val'
checkDuplicateLabels val'
let val'' = overTypes (desaturateAllTypeSynonyms . setifyAll) val'
ty' = varIfUnknown . desaturateAllTypeSynonyms . setifyAll $ ty
return (ident, (val'', ty'))
where
tidyUp (ts, sub) = map (\(i, (val, ty)) -> (i, (overTypes (sub $?) val, sub $? ty))) ts
checkMain nm ty = when (Just moduleName == mainModuleName && nm == Ident C.main) $ do
[eff, a] <- replicateM 2 fresh
ty =?= TypeApp (TypeApp (TypeConstructor (Qualified (Just (ModuleName [ProperName "Control", ProperName "Monad", ProperName "Eff"])) (ProperName "Eff"))) eff) a
type TypeData = M.Map (ModuleName, Ident) (Type, NameKind, NameVisibility)
type UntypedData = [(Ident, Type)]
typeDictionaryForBindingGroup :: ModuleName -> [(Ident, Expr)] -> UnifyT Type Check ([(Ident, Expr)], [(Ident, (Expr, Type, Bool))], TypeData, UntypedData)
typeDictionaryForBindingGroup moduleName vals = do
let
es = map isTyped vals
untyped = lefts es
typed = rights es
typedDict = map (\(ident, (_, ty, _)) -> (ident, ty)) typed
untypedNames <- replicateM (length untyped) fresh
let
untypedDict = zip (map fst untyped) untypedNames
dict = M.fromList (map (\(ident, ty) -> ((moduleName, ident), (ty, LocalVariable, Undefined))) $ typedDict ++ untypedDict)
return (untyped, typed, dict, untypedDict)
checkTypedBindingGroupElement :: ModuleName -> (Ident, (Expr, Type, Bool)) -> TypeData -> UnifyT Type Check (Ident, (Expr, Type))
checkTypedBindingGroupElement moduleName (ident, (val', ty, checkType)) dict = do
kind <- liftCheck $ kindOf moduleName ty
guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
val'' <- if checkType
then bindNames dict $ TypedValue True <$> check val' ty' <*> pure ty'
else return (TypedValue False val' ty')
return (ident, (val'', ty'))
typeForBindingGroupElement :: (Ident, Expr) -> TypeData -> UntypedData -> UnifyT Type Check (Ident, (Expr, Type))
typeForBindingGroupElement (ident, val) dict untypedDict = do
TypedValue _ val' ty <- bindNames dict $ infer val
ty =?= fromMaybe (error "name not found in dictionary") (lookup ident untypedDict)
return (ident, (TypedValue True val' ty, ty))
isTyped :: (Ident, Expr) -> (Either (Ident, Expr) (Ident, (Expr, Type, Bool)))
isTyped (name, TypedValue checkType value ty) = Right (name, (value, ty, checkType))
isTyped (name, value) = Left (name, value)
overTypes :: (Type -> Type) -> Expr -> Expr
overTypes f = let (_, f', _) = everywhereOnValues id g id in f'
where
g :: Expr -> Expr
g (TypedValue checkTy val t) = TypedValue checkTy val (f t)
g (TypeClassDictionary b (nm, tys) sco) = TypeClassDictionary b (nm, map f tys) sco
g other = other
replaceTypeClassDictionaries :: ModuleName -> Expr -> Check Expr
replaceTypeClassDictionaries mn =
let (_, f, _) = everywhereOnValuesTopDownM return go return
in f
where
go (TypeClassDictionary trySuperclasses constraint dicts) = do
env <- getEnv
entails env mn dicts constraint trySuperclasses
go other = return other
data DictionaryValue
= LocalDictionaryValue (Qualified Ident)
| GlobalDictionaryValue (Qualified Ident)
| DependentDictionaryValue (Qualified Ident) [DictionaryValue]
| SubclassDictionaryValue DictionaryValue (Qualified ProperName) Integer
deriving (Show, Ord, Eq)
entails :: Environment -> ModuleName -> [TypeClassDictionaryInScope] -> (Qualified ProperName, [Type]) -> Bool -> Check Expr
entails env moduleName context = solve (sortedNubBy canonicalizeDictionary (filter filterModule context))
where
sortedNubBy :: (Ord k) => (v -> k) -> [v] -> [v]
sortedNubBy f vs = M.elems (M.fromList (map (f &&& id) vs))
filterModule :: TypeClassDictionaryInScope -> Bool
filterModule (TypeClassDictionaryInScope { tcdName = Qualified (Just mn) _ }) | mn == moduleName = True
filterModule (TypeClassDictionaryInScope { tcdName = Qualified Nothing _ }) = True
filterModule _ = False
solve context' (className, tys) trySuperclasses =
checkOverlaps $ go trySuperclasses className tys
where
go trySuperclasses' className' tys' =
[ mkDictionary (canonicalizeDictionary tcd) args
| tcd <- context'
, className' == tcdClassName tcd
, subst <- maybeToList . (>>= verifySubstitution) . fmap concat $ zipWithM (typeHeadsAreEqual moduleName env) tys' (tcdInstanceTypes tcd)
, args <- solveSubgoals subst (tcdDependencies tcd) ] ++
[ SubclassDictionaryValue suDict superclass index
| trySuperclasses'
, (subclassName, (args, _, implies)) <- M.toList (typeClasses env)
, (index, (superclass, suTyArgs)) <- zip [0..] implies
, className' == superclass
, subst <- maybeToList . (>>= verifySubstitution) . fmap concat $ zipWithM (typeHeadsAreEqual moduleName env) tys' suTyArgs
, args' <- maybeToList $ mapM (flip lookup subst) (map fst args)
, suDict <- go True subclassName args' ]
solveSubgoals :: [(String, Type)] -> Maybe [(Qualified ProperName, [Type])] -> [Maybe [DictionaryValue]]
solveSubgoals _ Nothing = return Nothing
solveSubgoals subst (Just subgoals) = do
dict <- mapM (uncurry (go True) . second (map (replaceAllTypeVars subst))) subgoals
return $ Just dict
mkDictionary :: Qualified Ident -> Maybe [DictionaryValue] -> DictionaryValue
mkDictionary fnName Nothing = LocalDictionaryValue fnName
mkDictionary fnName (Just []) = GlobalDictionaryValue fnName
mkDictionary fnName (Just dicts) = DependentDictionaryValue fnName dicts
dictionaryValueToValue :: DictionaryValue -> Expr
dictionaryValueToValue (LocalDictionaryValue fnName) = Var fnName
dictionaryValueToValue (GlobalDictionaryValue fnName) = Var fnName
dictionaryValueToValue (DependentDictionaryValue fnName dicts) = foldl App (Var fnName) (map dictionaryValueToValue dicts)
dictionaryValueToValue (SubclassDictionaryValue dict superclassName index) =
App (Accessor (C.__superclass_ ++ show superclassName ++ "_" ++ show index)
(dictionaryValueToValue dict))
valUndefined
verifySubstitution :: [(String, Type)] -> Maybe [(String, Type)]
verifySubstitution subst = do
let grps = groupBy ((==) `on` fst) subst
guard (all (pairwise (unifiesWith env) . map snd) grps)
return $ map head grps
checkOverlaps :: [DictionaryValue] -> Check Expr
checkOverlaps dicts =
case [ (d1, d2) | d1 <- dicts, d2 <- dicts, d1 `overlapping` d2 ] of
(d1, d2) : _ -> throwError . strMsg $ unlines
[ "Overlapping instances found for " ++ show className ++ " " ++ unwords (map prettyPrintType tys) ++ "."
, "For example:"
, prettyPrintDictionaryValue d1
, "and:"
, prettyPrintDictionaryValue d2
]
_ -> case chooseSimplestDictionaries dicts of
[] -> throwError . strMsg $
"No instance found for " ++ show className ++ " " ++ unwords (map prettyPrintTypeAtom tys)
d : _ -> return $ dictionaryValueToValue d
chooseSimplestDictionaries :: [DictionaryValue] -> [DictionaryValue]
chooseSimplestDictionaries ds = case filter isSimpleDictionaryValue ds of
[] -> ds
simple -> simple
isSimpleDictionaryValue SubclassDictionaryValue{} = False
isSimpleDictionaryValue (DependentDictionaryValue _ ds) = all isSimpleDictionaryValue ds
isSimpleDictionaryValue _ = True
overlapping :: DictionaryValue -> DictionaryValue -> Bool
overlapping (LocalDictionaryValue nm1) (LocalDictionaryValue nm2) | nm1 == nm2 = False
overlapping (GlobalDictionaryValue nm1) (GlobalDictionaryValue nm2) | nm1 == nm2 = False
overlapping (DependentDictionaryValue nm1 ds1) (DependentDictionaryValue nm2 ds2)
| nm1 == nm2 = any id $ zipWith overlapping ds1 ds2
overlapping (SubclassDictionaryValue _ _ _) _ = False
overlapping _ (SubclassDictionaryValue _ _ _) = False
overlapping _ _ = True
prettyPrintDictionaryValue :: DictionaryValue -> String
prettyPrintDictionaryValue = unlines . indented 0
where
indented n (LocalDictionaryValue _) = [spaces n ++ "Dictionary in scope"]
indented n (GlobalDictionaryValue nm) = [spaces n ++ show nm]
indented n (DependentDictionaryValue nm args) = (spaces n ++ show nm ++ " via") : concatMap (indented (n + 2)) args
indented n (SubclassDictionaryValue sup nm _) = (spaces n ++ show nm ++ " via superclass") : indented (n + 2) sup
spaces n = replicate n ' ' ++ "- "
valUndefined :: Expr
valUndefined = Var (Qualified (Just (ModuleName [ProperName C.prim])) (Ident C.undefined))
pairwise :: (a -> a -> Bool) -> [a] -> Bool
pairwise _ [] = True
pairwise _ [_] = True
pairwise p (x : xs) = all (p x) xs && pairwise p xs
unifiesWith :: Environment -> Type -> Type -> Bool
unifiesWith _ (TUnknown u1) (TUnknown u2) | u1 == u2 = True
unifiesWith _ (Skolem _ s1 _) (Skolem _ s2 _) | s1 == s2 = True
unifiesWith _ (TypeVar v1) (TypeVar v2) | v1 == v2 = True
unifiesWith _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = True
unifiesWith e (TypeApp h1 t1) (TypeApp h2 t2) = unifiesWith e h1 h2 && unifiesWith e t1 t2
unifiesWith e (SaturatedTypeSynonym name args) t2 =
case expandTypeSynonym' e name args of
Left _ -> False
Right t1 -> unifiesWith e t1 t2
unifiesWith e t1 t2@(SaturatedTypeSynonym _ _) = unifiesWith e t2 t1
unifiesWith _ _ _ = False
typeHeadsAreEqual :: ModuleName -> Environment -> Type -> Type -> Maybe [(String, Type)]
typeHeadsAreEqual _ _ (Skolem _ s1 _) (Skolem _ s2 _) | s1 == s2 = Just []
typeHeadsAreEqual _ _ t (TypeVar v) = Just [(v, t)]
typeHeadsAreEqual _ _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = Just []
typeHeadsAreEqual m e (TypeApp h1 t1) (TypeApp h2 t2) = (++) <$> typeHeadsAreEqual m e h1 h2 <*> typeHeadsAreEqual m e t1 t2
typeHeadsAreEqual m e (SaturatedTypeSynonym name args) t2 = case expandTypeSynonym' e name args of
Left _ -> Nothing
Right t1 -> typeHeadsAreEqual m e t1 t2
typeHeadsAreEqual _ _ _ _ = Nothing
skolemEscapeCheck :: Expr -> Check ()
skolemEscapeCheck (TypedValue False _ _) = return ()
skolemEscapeCheck root@TypedValue{} =
let (_, f, _, _, _) = everythingWithContextOnValues [] [] (++) def go def def def
in case f root of
[] -> return ()
((binding, val) : _) -> throwError $ mkErrorStack ("Rigid/skolem type variable " ++ maybe "" (("bound by " ++) . prettyPrintValue) binding ++ " has escaped.") (Just (ExprError val))
where
def s _ = (s, [])
go :: [(SkolemScope, Expr)] -> Expr -> ([(SkolemScope, Expr)], [(Maybe Expr, Expr)])
go scos val@(TypedValue _ _ (ForAll _ _ (Just sco))) = ((sco, val) : scos, [])
go scos val@(TypedValue _ _ ty) = case collectSkolems ty \\ map fst scos of
(sco : _) -> (scos, [(findBindingScope sco, val)])
_ -> (scos, [])
where
collectSkolems :: Type -> [SkolemScope]
collectSkolems = nub . everythingOnTypes (++) collect
where
collect (Skolem _ _ scope) = [scope]
collect _ = []
go scos _ = (scos, [])
findBindingScope :: SkolemScope -> Maybe Expr
findBindingScope sco =
let (_, f, _, _, _) = everythingOnValues mappend (const mempty) go' (const mempty) (const mempty) (const mempty)
in getFirst $ f root
where
go' val@(TypedValue _ _ (ForAll _ _ (Just sco'))) | sco == sco' = First (Just val)
go' _ = mempty
skolemEscapeCheck val = throwError $ mkErrorStack "Untyped value passed to skolemEscapeCheck" (Just (ExprError val))
checkDuplicateLabels :: Expr -> Check ()
checkDuplicateLabels =
let (_, f, _) = everywhereOnValuesM def go def
in void . f
where
def :: a -> Check a
def = return
go :: Expr -> Check Expr
go e@(TypedValue _ _ ty) = checkDups ty >> return e
go other = return other
checkDups :: Type -> Check ()
checkDups (TypeApp t1 t2) = checkDups t1 >> checkDups t2
checkDups (SaturatedTypeSynonym _ ts) = mapM_ checkDups ts
checkDups (ForAll _ t _) = checkDups t
checkDups (ConstrainedType args t) = do
mapM_ (checkDups) $ concatMap snd args
checkDups t
checkDups r@(RCons _ _ _) =
let (ls, _) = rowToList r in
case firstDup . sort . map fst $ ls of
Just l -> throwError . strMsg $ "Duplicate label " ++ show l ++ " in row"
Nothing -> return ()
checkDups _ = return ()
firstDup :: (Eq a) => [a] -> Maybe a
firstDup (x : xs@(x' : _))
| x == x' = Just x
| otherwise = firstDup xs
firstDup _ = Nothing
setify :: Type -> Type
setify = rowFromList . first (M.toList . M.fromList) . rowToList
setifyAll :: Type -> Type
setifyAll = everywhereOnTypes setify
varIfUnknown :: Type -> Type
varIfUnknown ty =
let unks = nub $ unknowns ty
toName = (:) 't' . show
ty' = everywhereOnTypes typeToVar ty
typeToVar :: Type -> Type
typeToVar (TUnknown u) = TypeVar (toName u)
typeToVar t = t
in mkForAll (sort . map toName $ unks) ty'
instantiatePolyTypeWithUnknowns :: Expr -> Type -> UnifyT Type Check (Expr, Type)
instantiatePolyTypeWithUnknowns val (ForAll ident ty _) = do
ty' <- replaceVarWithUnknown ident ty
instantiatePolyTypeWithUnknowns val ty'
instantiatePolyTypeWithUnknowns val (ConstrainedType constraints ty) = do
dicts <- getTypeClassDictionaries
(_, ty') <- instantiatePolyTypeWithUnknowns (error "Types under a constraint cannot themselves be constrained") ty
return (foldl App val (map (flip (TypeClassDictionary True) dicts) constraints), ty')
instantiatePolyTypeWithUnknowns val ty = return (val, ty)
replaceVarWithUnknown :: String -> Type -> UnifyT Type Check Type
replaceVarWithUnknown ident ty = do
tu <- fresh
return $ replaceTypeVars ident tu ty
replaceAllTypeSynonyms' :: Environment -> Type -> Either String Type
replaceAllTypeSynonyms' env d =
let
syns = map (\(name, (args, _)) -> (name, length args)) . M.toList $ typeSynonyms env
in
saturateAllTypeSynonyms syns d
replaceAllTypeSynonyms :: (Error e, Functor m, Monad m, MonadState CheckState m, MonadError e m) => Type -> m Type
replaceAllTypeSynonyms d = do
env <- getEnv
either (throwError . strMsg) return $ replaceAllTypeSynonyms' env d
desaturateAllTypeSynonyms :: Type -> Type
desaturateAllTypeSynonyms = everywhereOnTypes replaceSaturatedTypeSynonym
where
replaceSaturatedTypeSynonym (SaturatedTypeSynonym name args) = foldl TypeApp (TypeConstructor name) args
replaceSaturatedTypeSynonym t = t
expandTypeSynonym' :: Environment -> Qualified ProperName -> [Type] -> Either String Type
expandTypeSynonym' env name args =
case M.lookup name (typeSynonyms env) of
Just (synArgs, body) -> do
let repl = replaceAllTypeVars (zip (map fst synArgs) args) body
replaceAllTypeSynonyms' env repl
Nothing -> error "Type synonym was not defined"
expandTypeSynonym :: (Error e, Functor m, Monad m, MonadState CheckState m, MonadError e m) => Qualified ProperName -> [Type] -> m Type
expandTypeSynonym name args = do
env <- getEnv
either (throwError . strMsg) return $ expandTypeSynonym' env name args
expandAllTypeSynonyms :: (Error e, Functor m, Applicative m, Monad m, MonadState CheckState m, MonadError e m) => Type -> m Type
expandAllTypeSynonyms = everywhereOnTypesTopDownM go
where
go (SaturatedTypeSynonym name args) = expandTypeSynonym name args
go other = return other
ensureNoDuplicateProperties :: (Error e, MonadError e m) => [(String, Expr)] -> m ()
ensureNoDuplicateProperties ps = guardWith (strMsg "Duplicate property names") $ length (nub . map fst $ ps) == length ps
infer :: Expr -> UnifyT Type Check Expr
infer val = rethrow (mkErrorStack "Error inferring type of value" (Just (ExprError val)) <>) $ infer' val
infer' :: Expr -> UnifyT Type Check Expr
infer' v@(NumericLiteral _) = return $ TypedValue True v tyNumber
infer' v@(StringLiteral _) = return $ TypedValue True v tyString
infer' v@(BooleanLiteral _) = return $ TypedValue True v tyBoolean
infer' (ArrayLiteral vals) = do
ts <- mapM infer vals
els <- fresh
forM_ ts $ \(TypedValue _ _ t) -> els =?= t
return $ TypedValue True (ArrayLiteral ts) (TypeApp tyArray els)
infer' (ObjectLiteral ps) = do
ensureNoDuplicateProperties ps
ts <- mapM (infer . snd) ps
let fields = zipWith (\name (TypedValue _ _ t) -> (name, t)) (map fst ps) ts
ty = TypeApp tyObject $ rowFromList (fields, REmpty)
return $ TypedValue True (ObjectLiteral (zip (map fst ps) ts)) ty
infer' (ObjectUpdate o ps) = do
ensureNoDuplicateProperties ps
row <- fresh
newVals <- zipWith (\(name, _) t -> (name, t)) ps <$> mapM (infer . snd) ps
let newTys = map (\(name, TypedValue _ _ ty) -> (name, ty)) newVals
oldTys <- zip (map fst ps) <$> replicateM (length ps) fresh
let oldTy = TypeApp tyObject $ rowFromList (oldTys, row)
o' <- TypedValue True <$> check o oldTy <*> pure oldTy
return $ TypedValue True (ObjectUpdate o' newVals) $ TypeApp tyObject $ rowFromList (newTys, row)
infer' (Accessor prop val) = do
typed@(TypedValue _ _ objTy) <- infer val
propTy <- inferProperty objTy prop
case propTy of
Nothing -> do
field <- fresh
rest <- fresh
_ <- subsumes Nothing objTy (TypeApp tyObject (RCons prop field rest))
return $ TypedValue True (Accessor prop typed) field
Just ty -> return $ TypedValue True (Accessor prop typed) ty
infer' (Abs (Left arg) ret) = do
ty <- fresh
Just moduleName <- checkCurrentModule <$> get
makeBindingGroupVisible $ bindLocalVariables moduleName [(arg, ty, Defined)] $ do
body@(TypedValue _ _ bodyTy) <- infer' ret
return $ TypedValue True (Abs (Left arg) body) $ function ty bodyTy
infer' (Abs (Right _) _) = error "Binder was not desugared"
infer' (App f arg) = do
f'@(TypedValue _ _ ft) <- infer f
(ret, app) <- checkFunctionApplication f' ft arg Nothing
return $ TypedValue True app ret
infer' (Var var) = do
Just moduleName <- checkCurrentModule <$> get
checkVisibility moduleName var
ty <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< lookupVariable moduleName $ var
case ty of
ConstrainedType constraints ty' -> do
dicts <- getTypeClassDictionaries
return $ TypedValue True (foldl App (Var var) (map (flip (TypeClassDictionary True) dicts) constraints)) ty'
_ -> return $ TypedValue True (Var var) ty
infer' v@(Constructor c) = do
env <- getEnv
case M.lookup c (dataConstructors env) of
Nothing -> throwError . strMsg $ "Constructor " ++ show c ++ " is undefined"
Just (_, _, ty) -> do ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
return $ TypedValue True v ty'
infer' (Case vals binders) = do
ts <- mapM infer vals
ret <- fresh
binders' <- checkBinders (map (\(TypedValue _ _ t) -> t) ts) ret binders
return $ TypedValue True (Case ts binders') ret
infer' (IfThenElse cond th el) = do
cond' <- check cond tyBoolean
v2@(TypedValue _ _ t2) <- infer th
v3@(TypedValue _ _ t3) <- infer el
(v2', v3', t) <- meet v2 v3 t2 t3
return $ TypedValue True (IfThenElse cond' v2' v3') t
infer' (Let ds val) = do
(ds', val'@(TypedValue _ _ valTy)) <- inferLetBinding [] ds val infer
return $ TypedValue True (Let ds' val') valTy
infer' (SuperClassDictionary className tys) = do
dicts <- getTypeClassDictionaries
return $ TypeClassDictionary False (className, tys) dicts
infer' (TypedValue checkType val ty) = do
Just moduleName <- checkCurrentModule <$> get
kind <- liftCheck $ kindOf moduleName ty
guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
val' <- if checkType then check val ty' else return val
return $ TypedValue True val' ty'
infer' (PositionedValue pos val) = rethrowWithPosition pos $ infer' val
infer' _ = error "Invalid argument to infer"
inferLetBinding :: [Declaration] -> [Declaration] -> Expr -> (Expr -> UnifyT Type Check Expr) -> UnifyT Type Check ([Declaration], Expr)
inferLetBinding seen [] ret j = (,) seen <$> makeBindingGroupVisible (j ret)
inferLetBinding seen (ValueDeclaration ident nameKind [] Nothing tv@(TypedValue checkType val ty) : rest) ret j = do
Just moduleName <- checkCurrentModule <$> get
kind <- liftCheck $ kindOf moduleName ty
guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
let dict = M.singleton (moduleName, ident) (ty, nameKind, Undefined)
ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
TypedValue _ val' ty'' <- if checkType then bindNames dict (check val ty') else return tv
bindNames (M.singleton (moduleName, ident) (ty'', nameKind, Defined)) $ inferLetBinding (seen ++ [ValueDeclaration ident nameKind [] Nothing (TypedValue checkType val' ty'')]) rest ret j
inferLetBinding seen (ValueDeclaration ident nameKind [] Nothing val : rest) ret j = do
valTy <- fresh
Just moduleName <- checkCurrentModule <$> get
let dict = M.singleton (moduleName, ident) (valTy, nameKind, Undefined)
TypedValue _ val' valTy' <- bindNames dict $ infer val
valTy =?= valTy'
bindNames (M.singleton (moduleName, ident) (valTy', nameKind, Defined)) $ inferLetBinding (seen ++ [ValueDeclaration ident nameKind [] Nothing val']) rest ret j
inferLetBinding seen (BindingGroupDeclaration ds : rest) ret j = do
Just moduleName <- checkCurrentModule <$> get
(untyped, typed, dict, untypedDict) <- typeDictionaryForBindingGroup moduleName (map (\(i, _, v) -> (i, v)) ds)
ds1' <- parU typed $ \e -> checkTypedBindingGroupElement moduleName e dict
ds2' <- forM untyped $ \e -> typeForBindingGroupElement e dict untypedDict
let ds' = [(ident, LocalVariable, val') | (ident, (val', _)) <- ds1' ++ ds2']
makeBindingGroupVisible $ bindNames dict $ inferLetBinding (seen ++ [BindingGroupDeclaration ds']) rest ret j
inferLetBinding seen (PositionedDeclaration pos d : ds) ret j = rethrowWithPosition pos $ do
((d' : ds'), val') <- inferLetBinding seen (d : ds) ret j
return (PositionedDeclaration pos d' : ds', val')
inferLetBinding _ _ _ _ = error "Invalid argument to inferLetBinding"
inferProperty :: Type -> String -> UnifyT Type Check (Maybe Type)
inferProperty (TypeApp obj row) prop | obj == tyObject = do
let (props, _) = rowToList row
return $ lookup prop props
inferProperty (SaturatedTypeSynonym name args) prop = do
replaced <- introduceSkolemScope <=< expandTypeSynonym name $ args
inferProperty replaced prop
inferProperty (ForAll ident ty _) prop = do
replaced <- replaceVarWithUnknown ident ty
inferProperty replaced prop
inferProperty _ _ = return Nothing
inferBinder :: Type -> Binder -> UnifyT Type Check (M.Map Ident Type)
inferBinder _ NullBinder = return M.empty
inferBinder val (StringBinder _) = val =?= tyString >> return M.empty
inferBinder val (NumberBinder _) = val =?= tyNumber >> return M.empty
inferBinder val (BooleanBinder _) = val =?= tyBoolean >> return M.empty
inferBinder val (VarBinder name) = return $ M.singleton name val
inferBinder val (ConstructorBinder ctor binders) = do
env <- getEnv
case M.lookup ctor (dataConstructors env) of
Just (_, _, ty) -> do
(_, fn) <- instantiatePolyTypeWithUnknowns (error "Data constructor types cannot contain constraints") ty
fn' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ fn
go binders fn'
where
go [] ty' = do
_ <- subsumes Nothing val ty'
return M.empty
go (binder : binders') (TypeApp (TypeApp t obj) ret) | t == tyFunction =
M.union <$> inferBinder obj binder <*> go binders' ret
go _ _ = throwError . strMsg $ "Wrong number of arguments to constructor " ++ show ctor
_ -> throwError . strMsg $ "Constructor " ++ show ctor ++ " is not defined"
inferBinder val (ObjectBinder props) = do
row <- fresh
rest <- fresh
m1 <- inferRowProperties row rest props
val =?= TypeApp tyObject row
return m1
where
inferRowProperties :: Type -> Type -> [(String, Binder)] -> UnifyT Type Check (M.Map Ident Type)
inferRowProperties nrow row [] = nrow =?= row >> return M.empty
inferRowProperties nrow row ((name, binder):binders) = do
propTy <- fresh
m1 <- inferBinder propTy binder
m2 <- inferRowProperties nrow (RCons name propTy row) binders
return $ m1 `M.union` m2
inferBinder val (ArrayBinder binders) = do
el <- fresh
m1 <- M.unions <$> mapM (inferBinder el) binders
val =?= TypeApp tyArray el
return m1
inferBinder val (ConsBinder headBinder tailBinder) = do
el <- fresh
m1 <- inferBinder el headBinder
m2 <- inferBinder val tailBinder
val =?= TypeApp tyArray el
return $ m1 `M.union` m2
inferBinder val (NamedBinder name binder) = do
m <- inferBinder val binder
return $ M.insert name val m
inferBinder val (PositionedBinder pos binder) =
rethrowWithPosition pos $ inferBinder val binder
checkBinders :: [Type] -> Type -> [CaseAlternative] -> UnifyT Type Check [CaseAlternative]
checkBinders _ _ [] = return []
checkBinders nvals ret (CaseAlternative binders grd val : bs) = do
guardWith (strMsg "Overlapping binders in case statement") $
let ns = concatMap binderNames binders in length (nub ns) == length ns
Just moduleName <- checkCurrentModule <$> get
m1 <- M.unions <$> zipWithM inferBinder nvals binders
r <- bindLocalVariables moduleName [ (name, ty, Defined) | (name, ty) <- M.toList m1 ] $ do
val' <- TypedValue True <$> check val ret <*> pure ret
case grd of
Nothing -> return $ CaseAlternative binders Nothing val'
Just g -> do
g' <- check g tyBoolean
return $ CaseAlternative binders (Just g') val'
rs <- checkBinders nvals ret bs
return $ r : rs
newSkolemConstant :: UnifyT Type Check Int
newSkolemConstant = fresh'
newSkolemScope :: UnifyT Type Check SkolemScope
newSkolemScope = SkolemScope <$> fresh'
skolemize :: String -> Int -> SkolemScope -> Type -> Type
skolemize ident sko scope = replaceTypeVars ident (Skolem ident sko scope)
skolemizeTypesInValue :: String -> Int -> SkolemScope -> Expr -> Expr
skolemizeTypesInValue ident sko scope = let (_, f, _) = everywhereOnValues id go id in f
where
go (SuperClassDictionary c ts) = SuperClassDictionary c (map (skolemize ident sko scope) ts)
go other = other
introduceSkolemScope :: Type -> UnifyT Type Check Type
introduceSkolemScope = everywhereOnTypesM go
where
go (ForAll ident ty Nothing) = ForAll ident ty <$> (Just <$> newSkolemScope)
go other = return other
check :: Expr -> Type -> UnifyT Type Check Expr
check val ty = rethrow (mkErrorStack errorMessage (Just (ExprError val)) <>) $ check' val ty
where
errorMessage =
"Error checking type of term " ++
prettyPrintValue val ++
" against type " ++
prettyPrintType ty
check' :: Expr -> Type -> UnifyT Type Check Expr
check' val (ForAll ident ty _) = do
scope <- newSkolemScope
sko <- newSkolemConstant
let sk = skolemize ident sko scope ty
let skVal = skolemizeTypesInValue ident sko scope val
val' <- check skVal sk
return $ TypedValue True val' (ForAll ident ty (Just scope))
check' val t@(ConstrainedType constraints ty) = do
dictNames <- forM constraints $ \(Qualified _ (ProperName className), _) -> do
n <- liftCheck freshDictionaryName
return $ Ident $ "__dict_" ++ className ++ "_" ++ show n
val' <- makeBindingGroupVisible $ withTypeClassDictionaries (zipWith (\name (className, instanceTy) ->
TypeClassDictionaryInScope name className instanceTy Nothing TCDRegular False) (map (Qualified Nothing) dictNames)
constraints) $ check val ty
return $ TypedValue True (foldr (Abs . Left) val' dictNames) t
check' val (SaturatedTypeSynonym name args) = do
ty <- introduceSkolemScope <=< expandTypeSynonym name $ args
check val ty
check' val u@(TUnknown _) = do
val'@(TypedValue _ _ ty) <- infer val
(val'', ty') <- instantiatePolyTypeWithUnknowns val' ty
ty' =?= u
return $ TypedValue True val'' ty'
check' v@(NumericLiteral _) t | t == tyNumber =
return $ TypedValue True v t
check' v@(StringLiteral _) t | t == tyString =
return $ TypedValue True v t
check' v@(BooleanLiteral _) t | t == tyBoolean =
return $ TypedValue True v t
check' (ArrayLiteral vals) t@(TypeApp a ty) = do
a =?= tyArray
array <- ArrayLiteral <$> forM vals (`check` ty)
return $ TypedValue True array t
check' (Abs (Left arg) ret) ty@(TypeApp (TypeApp t argTy) retTy) | t == tyFunction = do
Just moduleName <- checkCurrentModule <$> get
ret' <- makeBindingGroupVisible $ bindLocalVariables moduleName [(arg, argTy, Defined)] $ check ret retTy
return $ TypedValue True (Abs (Left arg) ret') ty
check' (Abs (Right _) _) _ = error "Binder was not desugared"
check' (App f arg) ret = do
f'@(TypedValue _ _ ft) <- infer f
(_, app) <- checkFunctionApplication f' ft arg (Just ret)
return $ TypedValue True app ret
check' v@(Var var) ty = do
Just moduleName <- checkCurrentModule <$> get
checkVisibility moduleName var
repl <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< lookupVariable moduleName $ var
ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
v' <- subsumes (Just v) repl ty'
case v' of
Nothing -> throwError . strMsg $ "Unable to check type subsumption"
Just v'' -> return $ TypedValue True v'' ty'
check' (SuperClassDictionary className tys) _ = do
dicts <- getTypeClassDictionaries
return $ TypeClassDictionary False (className, tys) dicts
check' (TypedValue checkType val ty1) ty2 = do
Just moduleName <- checkCurrentModule <$> get
kind <- liftCheck $ kindOf moduleName ty1
guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
ty1' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty1
ty2' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty2
val' <- subsumes (Just val) ty1' ty2'
case val' of
Nothing -> throwError . strMsg $ "Unable to check type subsumption"
Just val'' -> do
val''' <- if checkType then check val'' ty2' else return val''
return $ TypedValue checkType (TypedValue True val''' ty1') ty2'
check' (Case vals binders) ret = do
vals' <- mapM infer vals
let ts = map (\(TypedValue _ _ t) -> t) vals'
binders' <- checkBinders ts ret binders
return $ TypedValue True (Case vals' binders') ret
check' (IfThenElse cond th el) ty = do
cond' <- check cond tyBoolean
th' <- check th ty
el' <- check el ty
return $ TypedValue True (IfThenElse cond' th' el') ty
check' (ObjectLiteral ps) t@(TypeApp obj row) | obj == tyObject = do
ensureNoDuplicateProperties ps
ps' <- checkProperties ps row False
return $ TypedValue True (ObjectLiteral ps') t
check' (TypeClassDictionaryConstructorApp name ps) t = do
ps' <- check' ps t
return $ TypedValue True (TypeClassDictionaryConstructorApp name ps') t
check' (ObjectUpdate obj ps) t@(TypeApp o row) | o == tyObject = do
ensureNoDuplicateProperties ps
us <- zip (map fst ps) <$> replicateM (length ps) fresh
let (propsToCheck, rest) = rowToList row
propsToRemove = map fst ps
remainingProps = filter (\(p, _) -> p `notElem` propsToRemove) propsToCheck
obj' <- check obj (TypeApp tyObject (rowFromList (us ++ remainingProps, rest)))
ps' <- checkProperties ps row True
return $ TypedValue True (ObjectUpdate obj' ps') t
check' (Accessor prop val) ty = do
rest <- fresh
val' <- check val (TypeApp tyObject (RCons prop ty rest))
return $ TypedValue True (Accessor prop val') ty
check' (Constructor c) ty = do
env <- getEnv
case M.lookup c (dataConstructors env) of
Nothing -> throwError . strMsg $ "Constructor " ++ show c ++ " is undefined"
Just (_, _, ty1) -> do
repl <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty1
_ <- subsumes Nothing repl ty
return $ TypedValue True (Constructor c) ty
check' (Let ds val) ty = do
(ds', val') <- inferLetBinding [] ds val (flip check ty)
return $ TypedValue True (Let ds' val') ty
check' val ty | containsTypeSynonyms ty = do
ty' <- introduceSkolemScope <=< expandAllTypeSynonyms $ ty
check val ty'
check' val kt@(KindedType ty kind) = do
guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
val' <- check' val ty
return $ TypedValue True val' kt
check' (PositionedValue pos val) ty =
rethrowWithPosition pos $ check val ty
check' val ty = throwError $ mkErrorStack ("Expr does not have type " ++ prettyPrintType ty) (Just (ExprError val))
containsTypeSynonyms :: Type -> Bool
containsTypeSynonyms = everythingOnTypes (||) go where
go (SaturatedTypeSynonym _ _) = True
go _ = False
checkProperties :: [(String, Expr)] -> Type -> Bool -> UnifyT Type Check [(String, Expr)]
checkProperties ps row lax = let (ts, r') = rowToList row in go ps ts r' where
go [] [] REmpty = return []
go [] [] u@(TUnknown _) = do u =?= REmpty
return []
go [] [] (Skolem _ _ _) | lax = return []
go [] ((p, _): _) _ | lax = return []
| otherwise = throwError $ mkErrorStack ("Object does not have property " ++ p) (Just (ExprError (ObjectLiteral ps)))
go ((p,_):_) [] REmpty = throwError $ mkErrorStack ("Property " ++ p ++ " is not present in closed object type " ++ prettyPrintRow row) (Just (ExprError (ObjectLiteral ps)))
go ((p,v):ps') [] u@(TUnknown _) = do
v'@(TypedValue _ _ ty) <- infer v
rest <- fresh
u =?= RCons p ty rest
ps'' <- go ps' [] rest
return $ (p, v') : ps''
go ((p,v):ps') ts r =
case lookup p ts of
Nothing -> do
v'@(TypedValue _ _ ty) <- infer v
rest <- fresh
r =?= RCons p ty rest
ps'' <- go ps' ts rest
return $ (p, v') : ps''
Just ty -> do
v' <- check v ty
ps'' <- go ps' (delete (p, ty) ts) r
return $ (p, v') : ps''
go _ _ _ = throwError $ mkErrorStack ("Object does not have type " ++ prettyPrintType (TypeApp tyObject row)) (Just (ExprError (ObjectLiteral ps)))
checkFunctionApplication :: Expr -> Type -> Expr -> Maybe Type -> UnifyT Type Check (Type, Expr)
checkFunctionApplication fn fnTy arg ret = rethrow (mkErrorStack errorMessage (Just (ExprError fn)) <>) $ do
subst <- unifyCurrentSubstitution <$> UnifyT get
checkFunctionApplication' fn (subst $? fnTy) arg (($?) subst <$> ret)
where
errorMessage = "Error applying function of type "
++ prettyPrintType fnTy
++ " to argument " ++ prettyPrintValue arg
checkFunctionApplication' :: Expr -> Type -> Expr -> Maybe Type -> UnifyT Type Check (Type, Expr)
checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg ret = do
tyFunction' =?= tyFunction
arg' <- check arg argTy
case ret of
Nothing -> return (retTy, App fn arg')
Just ret' -> do
Just app' <- subsumes (Just (App fn arg')) retTy ret'
return (retTy, app')
checkFunctionApplication' fn (ForAll ident ty _) arg ret = do
replaced <- replaceVarWithUnknown ident ty
checkFunctionApplication fn replaced arg ret
checkFunctionApplication' fn u@(TUnknown _) arg ret = do
arg' <- do
TypedValue _ arg' t <- infer arg
(arg'', t') <- instantiatePolyTypeWithUnknowns arg' t
return $ TypedValue True arg'' t'
let ty = (\(TypedValue _ _ t) -> t) arg'
ret' <- maybe fresh return ret
u =?= function ty ret'
return (ret', App fn arg')
checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) arg ret = do
ty <- introduceSkolemScope <=< expandTypeSynonym name $ tyArgs
checkFunctionApplication fn ty arg ret
checkFunctionApplication' fn (KindedType ty _) arg ret = do
checkFunctionApplication fn ty arg ret
checkFunctionApplication' fn (ConstrainedType constraints fnTy) arg ret = do
dicts <- getTypeClassDictionaries
checkFunctionApplication' (foldl App fn (map (flip (TypeClassDictionary True) dicts) constraints)) fnTy arg ret
checkFunctionApplication' fn fnTy dict@(TypeClassDictionary _ _ _) _ =
return (fnTy, App fn dict)
checkFunctionApplication' _ fnTy arg _ = throwError . strMsg $ "Cannot apply a function of type "
++ prettyPrintType fnTy
++ " to argument " ++ prettyPrintValue arg
subsumes :: Maybe Expr -> Type -> Type -> UnifyT Type Check (Maybe Expr)
subsumes val ty1 ty2 = rethrow (mkErrorStack errorMessage (ExprError <$> val) <>) $ subsumes' val ty1 ty2
where
errorMessage = "Error checking that type "
++ prettyPrintType ty1
++ " subsumes type "
++ prettyPrintType ty2
subsumes' :: Maybe Expr -> Type -> Type -> UnifyT Type Check (Maybe Expr)
subsumes' val (ForAll ident ty1 _) ty2 = do
replaced <- replaceVarWithUnknown ident ty1
subsumes val replaced ty2
subsumes' val ty1 (ForAll ident ty2 sco) =
case sco of
Just sco' -> do
sko <- newSkolemConstant
let sk = skolemize ident sko sco' ty2
subsumes val ty1 sk
Nothing -> throwError . strMsg $ "Skolem variable scope is unspecified"
subsumes' val (TypeApp (TypeApp f1 arg1) ret1) (TypeApp (TypeApp f2 arg2) ret2) | f1 == tyFunction && f2 == tyFunction = do
_ <- subsumes Nothing arg2 arg1
_ <- subsumes Nothing ret1 ret2
return val
subsumes' val (SaturatedTypeSynonym name tyArgs) ty2 = do
ty1 <- introduceSkolemScope <=< expandTypeSynonym name $ tyArgs
subsumes val ty1 ty2
subsumes' val ty1 (SaturatedTypeSynonym name tyArgs) = do
ty2 <- introduceSkolemScope <=< expandTypeSynonym name $ tyArgs
subsumes val ty1 ty2
subsumes' val (KindedType ty1 _) ty2 = do
subsumes val ty1 ty2
subsumes' val ty1 (KindedType ty2 _) = do
subsumes val ty1 ty2
subsumes' (Just val) (ConstrainedType constraints ty1) ty2 = do
dicts <- getTypeClassDictionaries
subsumes' (Just $ foldl App val (map (flip (TypeClassDictionary True) dicts) constraints)) ty1 ty2
subsumes' val (TypeApp f1 r1) (TypeApp f2 r2) | f1 == tyObject && f2 == tyObject = do
let
(ts1, r1') = rowToList r1
(ts2, r2') = rowToList r2
ts1' = sortBy (comparing fst) ts1
ts2' = sortBy (comparing fst) ts2
go ts1' ts2' r1' r2'
return val
where
go [] ts2 r1' r2' = r1' =?= rowFromList (ts2, r2')
go ts1 [] r1' r2' = r2' =?= rowFromList (ts1, r1')
go ((p1, ty1) : ts1) ((p2, ty2) : ts2) r1' r2'
| p1 == p2 = do _ <- subsumes Nothing ty1 ty2
go ts1 ts2 r1' r2'
| p1 < p2 = do rest <- fresh
r2' =?= RCons p1 ty1 rest
go ts1 ((p2, ty2) : ts2) r1' rest
| otherwise = do rest <- fresh
r1' =?= RCons p2 ty2 rest
go ((p1, ty1) : ts1) ts2 rest r2'
subsumes' val ty1 ty2@(TypeApp obj _) | obj == tyObject = subsumes val ty2 ty1
subsumes' val ty1 ty2 = do
ty1 =?= ty2
return val
meet :: Expr -> Expr -> Type -> Type -> UnifyT Type Check (Expr, Expr, Type)
meet e1 e2 (ForAll ident t1 _) t2 = do
t1' <- replaceVarWithUnknown ident t1
meet e1 e2 t1' t2
meet e1 e2 t1 (ForAll ident t2 _) = do
t2' <- replaceVarWithUnknown ident t2
meet e1 e2 t1 t2'
meet e1 e2 t1 t2 = do
t1 =?= t2
return (e1, e2, t1)