module Language.PureScript.TypeChecker.Subsumption
( subsumes
) where
import Prelude.Compat
import Control.Monad (when)
import Control.Monad.Error.Class (MonadError(..))
import Control.Monad.State.Class (MonadState(..), gets)
import Data.Foldable (for_)
import Data.List (sortBy, uncons)
import Data.List.Ordered (minusBy')
import Data.Ord (comparing)
import Language.PureScript.AST
import Language.PureScript.Crash
import Language.PureScript.Environment
import Language.PureScript.Errors
import Language.PureScript.TypeChecker.Monad
import Language.PureScript.TypeChecker.Skolems
import Language.PureScript.TypeChecker.Unify
import Language.PureScript.Types
data Mode = Elaborate | NoElaborate
data ModeSing (mode :: Mode) where
SElaborate :: ModeSing 'Elaborate
SNoElaborate :: ModeSing 'NoElaborate
type family Coercion (mode :: Mode) where
Coercion 'Elaborate = Expr -> Expr
Coercion 'NoElaborate = ()
defaultCoercion :: ModeSing mode -> Coercion mode
defaultCoercion SElaborate = id
defaultCoercion SNoElaborate = ()
subsumes
:: (MonadError MultipleErrors m, MonadState CheckState m)
=> Type
-> Type
-> m (Expr -> Expr)
subsumes ty1 ty2 =
withErrorMessageHint (ErrorInSubsumption ty1 ty2) $
subsumes' SElaborate ty1 ty2
subsumes'
:: (MonadError MultipleErrors m, MonadState CheckState m)
=> ModeSing mode
-> Type
-> Type
-> m (Coercion mode)
subsumes' mode (ForAll ident ty1 _) ty2 = do
replaced <- replaceVarWithUnknown ident ty1
subsumes' mode replaced ty2
subsumes' mode ty1 (ForAll ident ty2 sco) =
case sco of
Just sco' -> do
sko <- newSkolemConstant
let sk = skolemize ident sko sco' Nothing ty2
subsumes' mode ty1 sk
Nothing -> internalError "subsumes: unspecified skolem scope"
subsumes' mode (TypeApp (TypeApp f1 arg1) ret1) (TypeApp (TypeApp f2 arg2) ret2) | f1 == tyFunction && f2 == tyFunction = do
subsumes' SNoElaborate arg2 arg1
subsumes' SNoElaborate ret1 ret2
return (defaultCoercion mode)
subsumes' mode (KindedType ty1 _) ty2 =
subsumes' mode ty1 ty2
subsumes' mode ty1 (KindedType ty2 _) =
subsumes' mode ty1 ty2
subsumes' SElaborate (ConstrainedType constraints ty1) ty2 = do
dicts <- getTypeClassDictionaries
hints <- gets checkHints
elaborate <- subsumes' SElaborate ty1 ty2
let addDicts val = foldl App val (map (\cs -> TypeClassDictionary cs dicts hints) constraints)
return (elaborate . addDicts)
subsumes' mode (TypeApp f1 r1) (TypeApp f2 r2) | f1 == tyRecord && f2 == tyRecord = do
let
(ts1, r1') = rowToList r1
(ts2, r2') = rowToList r2
ts1' = sortBy (comparing fst) ts1
ts2' = sortBy (comparing fst) ts2
when (r1' == REmpty)
(for_ (firstMissingProp ts2' ts1') (throwError . errorMessage . PropertyIsMissing . fst))
when (r2' == REmpty)
(for_ (firstMissingProp ts1' ts2') (throwError . errorMessage . AdditionalProperty . fst))
go ts1' ts2' r1' r2'
return (defaultCoercion mode)
where
go [] ts2 r1' r2' = unifyTypes r1' (rowFromList (ts2, r2'))
go ts1 [] r1' r2' = unifyTypes r2' (rowFromList (ts1, r1'))
go ((p1, ty1) : ts1) ((p2, ty2) : ts2) r1' r2'
| p1 == p2 = do subsumes' SNoElaborate ty1 ty2
go ts1 ts2 r1' r2'
| p1 < p2 = do rest <- freshType
unifyTypes r2' (RCons p1 ty1 rest)
go ts1 ((p2, ty2) : ts2) r1' rest
| otherwise = do rest <- freshType
unifyTypes r1' (RCons p2 ty2 rest)
go ((p1, ty1) : ts1) ts2 rest r2'
firstMissingProp t1 t2 = fst <$> uncons (minusBy' (comparing fst) t1 t2)
subsumes' mode ty1 ty2@(TypeApp obj _) | obj == tyRecord =
subsumes' mode ty2 ty1
subsumes' mode ty1 ty2 = do
unifyTypes ty1 ty2
return (defaultCoercion mode)