module Language.PureScript.TypeChecker.TypeSearch
( typeSearch
) where
import Protolude
import Control.Monad.Writer (WriterT, runWriterT)
import qualified Data.Map as Map
import qualified Language.PureScript.TypeChecker.Entailment as Entailment
import qualified Language.PureScript.TypeChecker.Monad as TC
import Language.PureScript.TypeChecker.Subsumption
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
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)]
-> P.Environment
-> TC.CheckState
-> P.SourceType
-> P.SourceType
-> 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)
(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
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)])
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)]
-> P.Environment
-> TC.CheckState
-> P.SourceType
-> ([(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)