{-# LANGUAGE GADTs #-}
module Language.PureScript.TypeChecker.Subsumption
( subsumes
) where
import Prelude
import Control.Monad (when)
import Control.Monad.Error.Class (MonadError(..))
import Control.Monad.State.Class (MonadState(..))
import Data.Foldable (for_)
import Data.List (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 :: forall (mode :: Mode). ModeSing mode -> Coercion mode
defaultCoercion ModeSing mode
SElaborate = forall a. a -> a
id
defaultCoercion ModeSing mode
SNoElaborate = ()
subsumes
:: (MonadError MultipleErrors m, MonadState CheckState m)
=> SourceType
-> SourceType
-> m (Expr -> Expr)
subsumes :: forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m (Expr -> Expr)
subsumes SourceType
ty1 SourceType
ty2 =
forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m) =>
ErrorMessageHint -> m a -> m a
withErrorMessageHint (SourceType -> SourceType -> ErrorMessageHint
ErrorInSubsumption SourceType
ty1 SourceType
ty2) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) (mode :: Mode).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModeSing mode -> SourceType -> SourceType -> m (Coercion mode)
subsumes' ModeSing 'Elaborate
SElaborate SourceType
ty1 SourceType
ty2
subsumes'
:: (MonadError MultipleErrors m, MonadState CheckState m)
=> ModeSing mode
-> SourceType
-> SourceType
-> m (Coercion mode)
subsumes' :: forall (m :: * -> *) (mode :: Mode).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModeSing mode -> SourceType -> SourceType -> m (Coercion mode)
subsumes' ModeSing mode
mode (ForAll SourceAnn
_ Text
ident Maybe SourceType
mbK SourceType
ty1 Maybe SkolemScope
_) SourceType
ty2 = do
SourceType
u <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a.
(MonadError MultipleErrors m, HasCallStack) =>
Text -> m a
internalCompilerError Text
"Unelaborated forall") forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind Maybe SourceType
mbK
let replaced :: SourceType
replaced = forall a. Text -> Type a -> Type a -> Type a
replaceTypeVars Text
ident SourceType
u SourceType
ty1
forall (m :: * -> *) (mode :: Mode).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModeSing mode -> SourceType -> SourceType -> m (Coercion mode)
subsumes' ModeSing mode
mode SourceType
replaced SourceType
ty2
subsumes' ModeSing mode
mode SourceType
ty1 (ForAll SourceAnn
_ Text
ident Maybe SourceType
mbK SourceType
ty2 Maybe SkolemScope
sco) =
case Maybe SkolemScope
sco of
Just SkolemScope
sco' -> do
Int
sko <- forall (m :: * -> *). MonadState CheckState m => m Int
newSkolemConstant
let sk :: SourceType
sk = forall a.
a
-> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a -> Type a
skolemize SourceAnn
NullSourceAnn Text
ident Maybe SourceType
mbK Int
sko SkolemScope
sco' SourceType
ty2
forall (m :: * -> *) (mode :: Mode).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModeSing mode -> SourceType -> SourceType -> m (Coercion mode)
subsumes' ModeSing mode
mode SourceType
ty1 SourceType
sk
Maybe SkolemScope
Nothing -> forall a. HasCallStack => String -> a
internalError String
"subsumes: unspecified skolem scope"
subsumes' ModeSing mode
mode (TypeApp SourceAnn
_ (TypeApp SourceAnn
_ SourceType
f1 SourceType
arg1) SourceType
ret1) (TypeApp SourceAnn
_ (TypeApp SourceAnn
_ SourceType
f2 SourceType
arg2) SourceType
ret2) | forall a b. Type a -> Type b -> Bool
eqType SourceType
f1 SourceType
tyFunction Bool -> Bool -> Bool
&& forall a b. Type a -> Type b -> Bool
eqType SourceType
f2 SourceType
tyFunction = do
forall (m :: * -> *) (mode :: Mode).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModeSing mode -> SourceType -> SourceType -> m (Coercion mode)
subsumes' ModeSing 'NoElaborate
SNoElaborate SourceType
arg2 SourceType
arg1
forall (m :: * -> *) (mode :: Mode).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModeSing mode -> SourceType -> SourceType -> m (Coercion mode)
subsumes' ModeSing 'NoElaborate
SNoElaborate SourceType
ret1 SourceType
ret2
forall (m :: * -> *) a. Monad m => a -> m a
return (forall (mode :: Mode). ModeSing mode -> Coercion mode
defaultCoercion ModeSing mode
mode)
subsumes' ModeSing mode
mode (KindedType SourceAnn
_ SourceType
ty1 SourceType
_) SourceType
ty2 =
forall (m :: * -> *) (mode :: Mode).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModeSing mode -> SourceType -> SourceType -> m (Coercion mode)
subsumes' ModeSing mode
mode SourceType
ty1 SourceType
ty2
subsumes' ModeSing mode
mode SourceType
ty1 (KindedType SourceAnn
_ SourceType
ty2 SourceType
_) =
forall (m :: * -> *) (mode :: Mode).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModeSing mode -> SourceType -> SourceType -> m (Coercion mode)
subsumes' ModeSing mode
mode SourceType
ty1 SourceType
ty2
subsumes' ModeSing mode
SElaborate (ConstrainedType SourceAnn
_ Constraint SourceAnn
con SourceType
ty1) SourceType
ty2 = do
Map
QualifiedBy
(Map
(Qualified (ProperName 'ClassName))
(Map (Qualified Ident) (NonEmpty NamedDict)))
dicts <- forall (m :: * -> *).
MonadState CheckState m =>
m (Map
QualifiedBy
(Map
(Qualified (ProperName 'ClassName))
(Map (Qualified Ident) (NonEmpty NamedDict))))
getTypeClassDictionaries
[ErrorMessageHint]
hints <- forall (m :: * -> *).
MonadState CheckState m =>
m [ErrorMessageHint]
getHints
Expr -> Expr
elaborate <- forall (m :: * -> *) (mode :: Mode).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModeSing mode -> SourceType -> SourceType -> m (Coercion mode)
subsumes' ModeSing 'Elaborate
SElaborate SourceType
ty1 SourceType
ty2
let addDicts :: Expr -> Expr
addDicts Expr
val = Expr -> Expr -> Expr
App Expr
val (Constraint SourceAnn
-> Map
QualifiedBy
(Map
(Qualified (ProperName 'ClassName))
(Map (Qualified Ident) (NonEmpty NamedDict)))
-> [ErrorMessageHint]
-> Expr
TypeClassDictionary Constraint SourceAnn
con Map
QualifiedBy
(Map
(Qualified (ProperName 'ClassName))
(Map (Qualified Ident) (NonEmpty NamedDict)))
dicts [ErrorMessageHint]
hints)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr
elaborate forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
addDicts)
subsumes' ModeSing mode
mode (TypeApp SourceAnn
_ SourceType
f1 SourceType
r1) (TypeApp SourceAnn
_ SourceType
f2 SourceType
r2) | forall a b. Type a -> Type b -> Bool
eqType SourceType
f1 SourceType
tyRecord Bool -> Bool -> Bool
&& forall a b. Type a -> Type b -> Bool
eqType SourceType
f2 SourceType
tyRecord = do
let ([m ()]
common, (([RowListItem SourceAnn]
ts1', SourceType
r1'), ([RowListItem SourceAnn]
ts2', SourceType
r2'))) = forall a r.
(Type a -> Type a -> r)
-> Type a
-> Type a
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
alignRowsWith (forall (m :: * -> *) (mode :: Mode).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModeSing mode -> SourceType -> SourceType -> m (Coercion mode)
subsumes' ModeSing 'NoElaborate
SNoElaborate) SourceType
r1 SourceType
r2
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Type a -> Bool
isREmpty SourceType
r1')
(forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ (forall {a}.
[RowListItem a] -> [RowListItem a] -> Maybe (RowListItem a)
firstMissingProp [RowListItem SourceAnn]
ts2' [RowListItem SourceAnn]
ts1') (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleErrorMessage -> MultipleErrors
errorMessage forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label -> SimpleErrorMessage
PropertyIsMissing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. RowListItem a -> Label
rowListLabel))
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Type a -> Bool
isREmpty SourceType
r2')
(forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ (forall {a}.
[RowListItem a] -> [RowListItem a] -> Maybe (RowListItem a)
firstMissingProp [RowListItem SourceAnn]
ts1' [RowListItem SourceAnn]
ts2') (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleErrorMessage -> MultipleErrors
errorMessage forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label -> SimpleErrorMessage
AdditionalProperty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. RowListItem a -> Label
rowListLabel))
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [m ()]
common
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes (forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn]
ts1', SourceType
r1')) (forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem SourceAnn]
ts2', SourceType
r2'))
forall (m :: * -> *) a. Monad m => a -> m a
return (forall (mode :: Mode). ModeSing mode -> Coercion mode
defaultCoercion ModeSing mode
mode)
where
firstMissingProp :: [RowListItem a] -> [RowListItem a] -> Maybe (RowListItem a)
firstMissingProp [RowListItem a]
t1 [RowListItem a]
t2 = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [a] -> Maybe (a, [a])
uncons (forall a b. (a -> b -> Ordering) -> [a] -> [b] -> [a]
minusBy' (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing forall a. RowListItem a -> Label
rowListLabel) [RowListItem a]
t1 [RowListItem a]
t2)
subsumes' ModeSing mode
mode SourceType
ty1 ty2 :: SourceType
ty2@(TypeApp SourceAnn
_ SourceType
obj SourceType
_) | SourceType
obj forall a. Eq a => a -> a -> Bool
== SourceType
tyRecord =
forall (m :: * -> *) (mode :: Mode).
(MonadError MultipleErrors m, MonadState CheckState m) =>
ModeSing mode -> SourceType -> SourceType -> m (Coercion mode)
subsumes' ModeSing mode
mode SourceType
ty2 SourceType
ty1
subsumes' ModeSing mode
mode SourceType
ty1 SourceType
ty2 = do
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
ty1 SourceType
ty2
forall (m :: * -> *) a. Monad m => a -> m a
return (forall (mode :: Mode). ModeSing mode -> Coercion mode
defaultCoercion ModeSing mode
mode)