module Language.PureScript.TypeChecker.TypeSearch
  ( typeSearch
  ) where

import Protolude

import Control.Monad.Writer (WriterT, runWriterT)
import Data.Map qualified as Map
import Language.PureScript.TypeChecker.Entailment qualified as Entailment

import Language.PureScript.TypeChecker.Monad qualified as TC
import Language.PureScript.TypeChecker.Subsumption (subsumes)
import Language.PureScript.TypeChecker.Unify       as P

import Control.Monad.Supply                        as P
import Language.PureScript.AST                     as P
import Language.PureScript.Environment             as P
import Language.PureScript.Errors                  as P
import Language.PureScript.Label (Label)
import Language.PureScript.Names                   as P
import Language.PureScript.Pretty.Types            as P
import Language.PureScript.TypeChecker.Skolems     as Skolem
import Language.PureScript.TypeChecker.Synonyms    as P
import Language.PureScript.Types                   as P

checkInEnvironment
  :: Environment
  -> TC.CheckState
  -> StateT TC.CheckState (SupplyT (WriterT b (Except P.MultipleErrors))) a
  -> Maybe (a, Environment)
checkInEnvironment :: forall b a.
Environment
-> CheckState
-> StateT
     CheckState (SupplyT (WriterT b (Except MultipleErrors))) a
-> Maybe (a, Environment)
checkInEnvironment Environment
env CheckState
st =
  forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> b -> a
const forall a. Maybe a
Nothing) forall a. a -> Maybe a
Just
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e a. Except e a -> Either e a
runExcept
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) b r. Monad m => WriterT b m r -> m r
evalWriterT
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Functor m => Integer -> SupplyT m a -> m a
P.evalSupplyT Integer
0
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a.
Functor m =>
CheckState -> StateT CheckState m a -> m (a, Environment)
TC.runCheck (CheckState
st { checkEnv :: Environment
TC.checkEnv = Environment
env })

evalWriterT :: Monad m => WriterT b m r -> m r
evalWriterT :: forall (m :: * -> *) b r. Monad m => WriterT b m r -> m r
evalWriterT WriterT b m r
m = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst (forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT WriterT b m r
m)

checkSubsume
  :: Maybe [(P.Ident, Entailment.InstanceContext, P.SourceConstraint)]
  -- ^ Additional constraints we need to satisfy
  -> P.Environment
  -- ^ The Environment which contains the relevant definitions and typeclasses
  -> TC.CheckState
  -- ^ The typechecker state
  -> P.SourceType
  -- ^ The user supplied type
  -> P.SourceType
  -- ^ The type supplied by the environment
  -> Maybe ((P.Expr, [(P.Ident, Entailment.InstanceContext, P.SourceConstraint)]), P.Environment)
checkSubsume :: Maybe
  [(Ident,
    Map
      QualifiedBy
      (Map
         (Qualified (ProperName 'ClassName))
         (Map (Qualified Ident) (NonEmpty NamedDict))),
    SourceConstraint)]
-> Environment
-> CheckState
-> SourceType
-> SourceType
-> Maybe
     ((Expr,
       [(Ident,
         Map
           QualifiedBy
           (Map
              (Qualified (ProperName 'ClassName))
              (Map (Qualified Ident) (NonEmpty NamedDict))),
         SourceConstraint)]),
      Environment)
checkSubsume Maybe
  [(Ident,
    Map
      QualifiedBy
      (Map
         (Qualified (ProperName 'ClassName))
         (Map (Qualified Ident) (NonEmpty NamedDict))),
    SourceConstraint)]
unsolved Environment
env CheckState
st SourceType
userT SourceType
envT = forall b a.
Environment
-> CheckState
-> StateT
     CheckState (SupplyT (WriterT b (Except MultipleErrors))) a
-> Maybe (a, Environment)
checkInEnvironment Environment
env CheckState
st forall a b. (a -> b) -> a -> b
$ do
  let initializeSkolems :: SourceType
-> StateT
     CheckState
     (SupplyT (WriterT MultipleErrors (Except MultipleErrors)))
     SourceType
initializeSkolems =
        forall (m :: * -> *) a.
MonadState CheckState m =>
Type a -> m (Type a)
Skolem.introduceSkolemScope
        forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
P.replaceAllTypeSynonyms
        forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *).
(MonadWriter MultipleErrors m, MonadState CheckState m) =>
SourceType -> m SourceType
P.replaceTypeWildcards

  SourceType
userT' <- SourceType
-> StateT
     CheckState
     (SupplyT (WriterT MultipleErrors (Except MultipleErrors)))
     SourceType
initializeSkolems SourceType
userT
  SourceType
envT' <- SourceType
-> StateT
     CheckState
     (SupplyT (WriterT MultipleErrors (Except MultipleErrors)))
     SourceType
initializeSkolems SourceType
envT

  let dummyExpression :: Expr
dummyExpression = SourceSpan -> Qualified Ident -> Expr
P.Var SourceSpan
nullSourceSpan (forall a. QualifiedBy -> a -> Qualified a
P.Qualified QualifiedBy
P.ByNullSourcePos (Text -> Ident
P.Ident Text
"x"))

  Expr -> Expr
elab <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m (Expr -> Expr)
subsumes SourceType
envT' SourceType
userT'
  Substitution
subst <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Substitution
TC.checkSubstitution
  let expP :: Expr
expP = (SourceType -> SourceType) -> Expr -> Expr
P.overTypes (Substitution -> SourceType -> SourceType
P.substituteType Substitution
subst) (Expr -> Expr
elab Expr
dummyExpression)

  -- Now check that any unsolved constraints have not become impossible
  (forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_) (\(Ident
_, Map
  QualifiedBy
  (Map
     (Qualified (ProperName 'ClassName))
     (Map (Qualified Ident) (NonEmpty NamedDict)))
context, SourceConstraint
constraint) -> do
    let constraint' :: SourceConstraint
constraint' = forall a. ([Type a] -> [Type a]) -> Constraint a -> Constraint a
P.mapConstraintArgs (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map (Substitution -> SourceType -> SourceType
P.substituteType Substitution
subst)) SourceConstraint
constraint
    forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT forall k a. Map k a
Map.empty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) b r. Monad m => WriterT b m r -> m r
evalWriterT forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
 MonadWriter MultipleErrors m, MonadSupply m) =>
SolverOptions
-> SourceConstraint
-> Map
     QualifiedBy
     (Map
        (Qualified (ProperName 'ClassName))
        (Map (Qualified Ident) (NonEmpty NamedDict)))
-> [ErrorMessageHint]
-> WriterT
     (Any,
      [(Ident,
        Map
          QualifiedBy
          (Map
             (Qualified (ProperName 'ClassName))
             (Map (Qualified Ident) (NonEmpty NamedDict))),
        SourceConstraint)])
     (StateT
        (Map
           QualifiedBy
           (Map
              (Qualified (ProperName 'ClassName))
              (Map (Qualified Ident) (NonEmpty NamedDict))))
        m)
     Expr
Entailment.entails
        (Entailment.SolverOptions
          { solverShouldGeneralize :: Bool
solverShouldGeneralize = Bool
True
          , solverDeferErrors :: Bool
solverDeferErrors      = Bool
False
          }) SourceConstraint
constraint' Map
  QualifiedBy
  (Map
     (Qualified (ProperName 'ClassName))
     (Map (Qualified Ident) (NonEmpty NamedDict)))
context []) Maybe
  [(Ident,
    Map
      QualifiedBy
      (Map
         (Qualified (ProperName 'ClassName))
         (Map (Qualified Ident) (NonEmpty NamedDict))),
    SourceConstraint)]
unsolved

  -- Finally, check any constraints which were found during elaboration
  forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
 MonadWriter MultipleErrors m, MonadSupply m) =>
Bool
-> Expr
-> m (Expr,
      [(Ident,
        Map
          QualifiedBy
          (Map
             (Qualified (ProperName 'ClassName))
             (Map (Qualified Ident) (NonEmpty NamedDict))),
        SourceConstraint)])
Entailment.replaceTypeClassDictionaries (forall a. Maybe a -> Bool
isJust Maybe
  [(Ident,
    Map
      QualifiedBy
      (Map
         (Qualified (ProperName 'ClassName))
         (Map (Qualified Ident) (NonEmpty NamedDict))),
    SourceConstraint)]
unsolved) Expr
expP

accessorSearch
  :: Maybe [(P.Ident, Entailment.InstanceContext, P.SourceConstraint)]
  -> P.Environment
  -> TC.CheckState
  -> P.SourceType
  -> ([(Label, P.SourceType)], [(Label, P.SourceType)])
  -- ^ (all accessors we found, all accessors we found that match the result type)
accessorSearch :: Maybe
  [(Ident,
    Map
      QualifiedBy
      (Map
         (Qualified (ProperName 'ClassName))
         (Map (Qualified Ident) (NonEmpty NamedDict))),
    SourceConstraint)]
-> Environment
-> CheckState
-> SourceType
-> ([(Label, SourceType)], [(Label, SourceType)])
accessorSearch Maybe
  [(Ident,
    Map
      QualifiedBy
      (Map
         (Qualified (ProperName 'ClassName))
         (Map (Qualified Ident) (NonEmpty NamedDict))),
    SourceConstraint)]
unsolved Environment
env CheckState
st SourceType
userT = forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([], []) forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall b a.
Environment
-> CheckState
-> StateT
     CheckState (SupplyT (WriterT b (Except MultipleErrors))) a
-> Maybe (a, Environment)
checkInEnvironment Environment
env CheckState
st forall a b. (a -> b) -> a -> b
$ do
  let initializeSkolems :: SourceType
-> StateT
     CheckState
     (SupplyT (WriterT MultipleErrors (Except MultipleErrors)))
     SourceType
initializeSkolems =
        forall (m :: * -> *) a.
MonadState CheckState m =>
Type a -> m (Type a)
Skolem.introduceSkolemScope
        forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
P.replaceAllTypeSynonyms
        forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *).
(MonadWriter MultipleErrors m, MonadState CheckState m) =>
SourceType -> m SourceType
P.replaceTypeWildcards

  SourceType
userT' <- SourceType
-> StateT
     CheckState
     (SupplyT (WriterT MultipleErrors (Except MultipleErrors)))
     SourceType
initializeSkolems SourceType
userT

  SourceType
rowType <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind (SourceType -> SourceType
P.kindRow SourceType
P.kindType)
  SourceType
resultType <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind SourceType
P.kindType
  let recordFunction :: SourceType
recordFunction = SourceType -> SourceType -> SourceType
srcTypeApp (SourceType -> SourceType -> SourceType
srcTypeApp SourceType
tyFunction (SourceType -> SourceType -> SourceType
srcTypeApp SourceType
tyRecord SourceType
rowType)) SourceType
resultType
  Expr -> Expr
_ <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m (Expr -> Expr)
subsumes SourceType
recordFunction SourceType
userT'
  Substitution
subst <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Substitution
TC.checkSubstitution
  let solvedRow :: [(Label, SourceType)]
solvedRow = forall {a}. RowListItem a -> (Label, Type a)
toRowPair forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. (a, b) -> a
fst (forall a. Type a -> ([RowListItem a], Type a)
rowToList (Substitution -> SourceType -> SourceType
substituteType Substitution
subst SourceType
rowType))
  CheckState
tcS <- forall s (m :: * -> *). MonadState s m => m s
get
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Label, SourceType)]
solvedRow, forall a. (a -> Bool) -> [a] -> [a]
filter (\(Label, SourceType)
x -> CheckState -> SourceType -> (Label, SourceType) -> Bool
checkAccessor CheckState
tcS (Substitution -> SourceType -> SourceType
substituteType Substitution
subst SourceType
resultType) (Label, SourceType)
x) [(Label, SourceType)]
solvedRow)
  where
    checkAccessor :: CheckState -> SourceType -> (Label, SourceType) -> Bool
checkAccessor CheckState
tcs SourceType
x (Label
_, SourceType
type') = forall a. Maybe a -> Bool
isJust (Maybe
  [(Ident,
    Map
      QualifiedBy
      (Map
         (Qualified (ProperName 'ClassName))
         (Map (Qualified Ident) (NonEmpty NamedDict))),
    SourceConstraint)]
-> Environment
-> CheckState
-> SourceType
-> SourceType
-> Maybe
     ((Expr,
       [(Ident,
         Map
           QualifiedBy
           (Map
              (Qualified (ProperName 'ClassName))
              (Map (Qualified Ident) (NonEmpty NamedDict))),
         SourceConstraint)]),
      Environment)
checkSubsume Maybe
  [(Ident,
    Map
      QualifiedBy
      (Map
         (Qualified (ProperName 'ClassName))
         (Map (Qualified Ident) (NonEmpty NamedDict))),
    SourceConstraint)]
unsolved Environment
env CheckState
tcs SourceType
x SourceType
type')
    toRowPair :: RowListItem a -> (Label, Type a)
toRowPair (RowListItem a
_ Label
lbl Type a
ty) = (Label
lbl, Type a
ty)

typeSearch
  :: Maybe [(P.Ident, Entailment.InstanceContext, P.SourceConstraint)]
  -- ^ Additional constraints we need to satisfy
  -> P.Environment
  -- ^ The Environment which contains the relevant definitions and typeclasses
  -> TC.CheckState
  -- ^ The typechecker state
  -> P.SourceType
  -- ^ The type we are looking for
  -> ([(P.Qualified Text, P.SourceType)], Maybe [(Label, P.SourceType)])
typeSearch :: Maybe
  [(Ident,
    Map
      QualifiedBy
      (Map
         (Qualified (ProperName 'ClassName))
         (Map (Qualified Ident) (NonEmpty NamedDict))),
    SourceConstraint)]
-> Environment
-> CheckState
-> SourceType
-> ([(Qualified Text, SourceType)], Maybe [(Label, SourceType)])
typeSearch Maybe
  [(Ident,
    Map
      QualifiedBy
      (Map
         (Qualified (ProperName 'ClassName))
         (Map (Qualified Ident) (NonEmpty NamedDict))),
    SourceConstraint)]
unsolved Environment
env CheckState
st SourceType
type' =
  let
    runTypeSearch :: Map k P.SourceType -> Map k P.SourceType
    runTypeSearch :: forall k. Map k SourceType -> Map k SourceType
runTypeSearch = forall a b k. (a -> Maybe b) -> Map k a -> Map k b
Map.mapMaybe (\SourceType
ty -> Maybe
  [(Ident,
    Map
      QualifiedBy
      (Map
         (Qualified (ProperName 'ClassName))
         (Map (Qualified Ident) (NonEmpty NamedDict))),
    SourceConstraint)]
-> Environment
-> CheckState
-> SourceType
-> SourceType
-> Maybe
     ((Expr,
       [(Ident,
         Map
           QualifiedBy
           (Map
              (Qualified (ProperName 'ClassName))
              (Map (Qualified Ident) (NonEmpty NamedDict))),
         SourceConstraint)]),
      Environment)
checkSubsume Maybe
  [(Ident,
    Map
      QualifiedBy
      (Map
         (Qualified (ProperName 'ClassName))
         (Map (Qualified Ident) (NonEmpty NamedDict))),
    SourceConstraint)]
unsolved Environment
env CheckState
st SourceType
type' SourceType
ty forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> SourceType
ty)

    matchingNames :: Map (Qualified Ident) SourceType
matchingNames = forall k. Map k SourceType -> Map k SourceType
runTypeSearch (forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\(SourceType
ty, NameKind
_, NameVisibility
_) -> SourceType
ty) (Environment
-> Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
P.names Environment
env))
    matchingConstructors :: Map (Qualified (ProperName 'ConstructorName)) SourceType
matchingConstructors = forall k. Map k SourceType -> Map k SourceType
runTypeSearch (forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\(DataDeclType
_, ProperName 'TypeName
_, SourceType
ty, [Ident]
_) -> SourceType
ty) (Environment
-> Map
     (Qualified (ProperName 'ConstructorName))
     (DataDeclType, ProperName 'TypeName, SourceType, [Ident])
P.dataConstructors Environment
env))
    ([(Label, SourceType)]
allLabels, [(Label, SourceType)]
matchingLabels) = Maybe
  [(Ident,
    Map
      QualifiedBy
      (Map
         (Qualified (ProperName 'ClassName))
         (Map (Qualified Ident) (NonEmpty NamedDict))),
    SourceConstraint)]
-> Environment
-> CheckState
-> SourceType
-> ([(Label, SourceType)], [(Label, SourceType)])
accessorSearch Maybe
  [(Ident,
    Map
      QualifiedBy
      (Map
         (Qualified (ProperName 'ClassName))
         (Map (Qualified Ident) (NonEmpty NamedDict))),
    SourceConstraint)]
unsolved Environment
env CheckState
st SourceType
type'

    runPlainIdent :: (Qualified Ident, b) -> Maybe (Qualified Text, b)
runPlainIdent (Qualified QualifiedBy
m (Ident Text
k), b
v) = forall a. a -> Maybe a
Just (forall a. QualifiedBy -> a -> Qualified a
Qualified QualifiedBy
m Text
k, b
v)
    runPlainIdent (Qualified Ident, b)
_ = forall a. Maybe a
Nothing
  in
    ( (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (forall a. QualifiedBy -> a -> Qualified a
P.Qualified QualifiedBy
P.ByNullSourcePos forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text
"_." forall a. Semigroup a => a -> a -> a
<>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label -> Text
P.prettyPrintLabel) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Label, SourceType)]
matchingLabels)
      forall a. Semigroup a => a -> a -> a
<> forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall {b}. (Qualified Ident, b) -> Maybe (Qualified Text, b)
runPlainIdent (forall k a. Map k a -> [(k, a)]
Map.toList Map (Qualified Ident) SourceType
matchingNames)
      forall a. Semigroup a => a -> a -> a
<> (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map forall (a :: ProperNameType). ProperName a -> Text
P.runProperName) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Map k a -> [(k, a)]
Map.toList Map (Qualified (ProperName 'ConstructorName)) SourceType
matchingConstructors)
    , if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Label, SourceType)]
allLabels then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just [(Label, SourceType)]
allLabels)