{-# 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 (ErrorMessageHint(..), Expr(..), pattern NullSourceAnn)
import Language.PureScript.Crash (internalError)
import Language.PureScript.Environment (tyFunction, tyRecord)
import Language.PureScript.Errors (MultipleErrors, SimpleErrorMessage(..), errorMessage, internalCompilerError)
import Language.PureScript.TypeChecker.Monad (CheckState, getHints, getTypeClassDictionaries, withErrorMessageHint)
import Language.PureScript.TypeChecker.Skolems (newSkolemConstant, skolemize)
import Language.PureScript.TypeChecker.Unify (alignRowsWith, freshTypeWithKind, unifyTypes)
import Language.PureScript.Types (RowListItem(..), SourceType, Type(..), eqType, isREmpty, replaceTypeVars, rowFromList)
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
_ TypeVarVisibility
_ 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
_ TypeVarVisibility
_ 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 goWithLabel :: Label -> SourceType -> SourceType -> m ()
goWithLabel Label
l SourceType
t1 SourceType
t2 = forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m) =>
ErrorMessageHint -> m a -> m a
withErrorMessageHint (Label -> ErrorMessageHint
ErrorInRowLabel Label
l) 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 'NoElaborate
SNoElaborate SourceType
t1 SourceType
t2
let ([m ()]
common, (([RowListItem SourceAnn]
ts1', SourceType
r1'), ([RowListItem SourceAnn]
ts2', SourceType
r2'))) = forall a r.
(Label -> Type a -> Type a -> r)
-> Type a
-> Type a
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
alignRowsWith forall {m :: * -> *}.
(MonadState CheckState m, MonadError MultipleErrors m) =>
Label -> SourceType -> SourceType -> m ()
goWithLabel 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)