{-# LANGUAGE GADTs #-}

-- | Subsumption checking
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)

-- | Subsumption can operate in two modes:
--
-- * Elaboration mode, in which we try to insert type class dictionaries
-- * No-elaboration mode, in which we do not insert dictionaries
--
-- Some subsumption rules apply in both modes, and others are specific to
-- certain modes.
--
-- The subsumption algorithm follows the structure of the types in question,
-- and we can switch into no-elaboration mode when we move under a type
-- constructor where we can no longer insert dictionaries, e.g. into the fields
-- of a record.
data Mode = Elaborate | NoElaborate

-- | Value-level proxies for the two modes
data ModeSing (mode :: Mode) where
  SElaborate   :: ModeSing 'Elaborate
  SNoElaborate :: ModeSing 'NoElaborate

-- | This type family tracks what evidence we return from 'subsumes' for each
-- mode.
type family Coercion (mode :: Mode) where
  -- When elaborating, we generate a coercion
  Coercion 'Elaborate = Expr -> Expr
  -- When we're not elaborating, we don't generate coercions
  Coercion 'NoElaborate = ()

-- | The default coercion for each mode.
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 = ()

-- | Check that one type subsumes another, rethrowing errors to provide a better error message
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

-- | Check that one type subsumes another
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
  -- Nothing was elaborated, return the default coercion
  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
-- Only check subsumption for constrained types when elaborating.
-- Otherwise fall back to unification.
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
    -- For { ts1 | r1 } to subsume { ts2 | r2 } when r1 is empty (= we're working with a closed row),
    -- every property in ts2 must appear in ts1. If not, then the candidate expression is missing a required property.
    -- Conversely, when r2 is empty, every property in ts1 must appear in ts2, or else the expression has
    -- an additional property which is not allowed.
    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))
    -- Check subsumption for common labels
    forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [m ()]
common
    -- Inject the info here
    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'))
    -- Nothing was elaborated, return the default coercion
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall (mode :: Mode). ModeSing mode -> Coercion mode
defaultCoercion ModeSing mode
mode)
  where
    -- Find the first property that's in the first list (of tuples) but not in the second
    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
  -- Nothing was elaborated, return the default coercion
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall (mode :: Mode). ModeSing mode -> Coercion mode
defaultCoercion ModeSing mode
mode)