{-# 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
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

-- | 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
_ 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
  -- 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 ([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
    -- 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
    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)