module Language.PureScript.TypeChecker.Entailment
( InstanceContext
, SolverOptions(..)
, replaceTypeClassDictionaries
, newDictionaries
, entails
, findDicts
) where
import Prelude
import Protolude (ordNub)
import Control.Arrow (second, (&&&))
import Control.Monad.Error.Class (MonadError(..))
import Control.Monad.State (MonadState(..), MonadTrans(..), StateT(..), evalStateT, execStateT, foldM, gets, guard, join, modify, zipWithM, zipWithM_, (<=<))
import Control.Monad.Supply.Class (MonadSupply(..))
import Control.Monad.Writer (Any(..), MonadWriter(..), WriterT(..))
import Data.Either (lefts, partitionEithers)
import Data.Foldable (for_, fold, toList)
import Data.Function (on)
import Data.Functor (($>))
import Data.List (delete, findIndices, minimumBy, nubBy, sortOn, tails)
import Data.Maybe (catMaybes, fromMaybe, listToMaybe, mapMaybe)
import Data.Map qualified as M
import Data.Set qualified as S
import Data.Traversable (for)
import Data.Text (Text, stripPrefix, stripSuffix)
import Data.Text qualified as T
import Data.List.NonEmpty (NonEmpty(..))
import Data.List.NonEmpty qualified as NEL
import Language.PureScript.AST (Binder(..), ErrorMessageHint(..), Expr(..), Literal(..), pattern NullSourceSpan, everywhereOnValuesTopDownM, nullSourceSpan)
import Language.PureScript.Crash (internalError)
import Language.PureScript.Environment (Environment(..), FunctionalDependency(..), TypeClassData(..), dictTypeName, kindRow, tyBoolean, tyInt, tyString)
import Language.PureScript.Errors (MultipleErrors, SimpleErrorMessage(..), addHint, addHints, errorMessage, rethrow)
import Language.PureScript.Names (pattern ByNullSourcePos, Ident(..), ModuleName, ProperName(..), ProperNameType(..), Qualified(..), QualifiedBy(..), byMaybeModuleName, coerceProperName, disqualify, freshIdent, getQual)
import Language.PureScript.TypeChecker.Entailment.Coercible (GivenSolverState(..), WantedSolverState(..), initialGivenSolverState, initialWantedSolverState, insoluble, solveGivens, solveWanteds)
import Language.PureScript.TypeChecker.Entailment.IntCompare (mkFacts, mkRelation, solveRelation)
import Language.PureScript.TypeChecker.Kinds (elaborateKind, unifyKinds')
import Language.PureScript.TypeChecker.Monad (CheckState(..), withErrorMessageHint)
import Language.PureScript.TypeChecker.Synonyms (replaceAllTypeSynonyms)
import Language.PureScript.TypeChecker.Unify (freshTypeWithKind, substituteType, unifyTypes)
import Language.PureScript.TypeClassDictionaries (NamedDict, TypeClassDictionaryInScope(..), superclassName)
import Language.PureScript.Types
import Language.PureScript.Label (Label(..))
import Language.PureScript.PSString (PSString, mkString, decodeString)
import Language.PureScript.Constants.Libs qualified as C
import Language.PureScript.Constants.Prim qualified as C
data Evidence
= NamedInstance (Qualified Ident)
| WarnInstance SourceType
| IsSymbolInstance PSString
| ReflectableInstance Reflectable
| EmptyClassInstance
deriving (Int -> Evidence -> ShowS
[Evidence] -> ShowS
Evidence -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Evidence] -> ShowS
$cshowList :: [Evidence] -> ShowS
show :: Evidence -> String
$cshow :: Evidence -> String
showsPrec :: Int -> Evidence -> ShowS
$cshowsPrec :: Int -> Evidence -> ShowS
Show, Evidence -> Evidence -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Evidence -> Evidence -> Bool
$c/= :: Evidence -> Evidence -> Bool
== :: Evidence -> Evidence -> Bool
$c== :: Evidence -> Evidence -> Bool
Eq)
data Reflectable
= ReflectableInt Integer
| ReflectableString PSString
| ReflectableBoolean Bool
| ReflectableOrdering Ordering
deriving (Int -> Reflectable -> ShowS
[Reflectable] -> ShowS
Reflectable -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Reflectable] -> ShowS
$cshowList :: [Reflectable] -> ShowS
show :: Reflectable -> String
$cshow :: Reflectable -> String
showsPrec :: Int -> Reflectable -> ShowS
$cshowsPrec :: Int -> Reflectable -> ShowS
Show, Reflectable -> Reflectable -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Reflectable -> Reflectable -> Bool
$c/= :: Reflectable -> Reflectable -> Bool
== :: Reflectable -> Reflectable -> Bool
$c== :: Reflectable -> Reflectable -> Bool
Eq)
asExpression :: Reflectable -> Expr
asExpression :: Reflectable -> Expr
asExpression = \case
ReflectableInt Integer
n -> SourceSpan -> Literal Expr -> Expr
Literal SourceSpan
NullSourceSpan forall a b. (a -> b) -> a -> b
$ forall a. Either Integer Double -> Literal a
NumericLiteral forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left Integer
n
ReflectableString PSString
s -> SourceSpan -> Literal Expr -> Expr
Literal SourceSpan
NullSourceSpan forall a b. (a -> b) -> a -> b
$ forall a. PSString -> Literal a
StringLiteral PSString
s
ReflectableBoolean Bool
b -> SourceSpan -> Literal Expr -> Expr
Literal SourceSpan
NullSourceSpan forall a b. (a -> b) -> a -> b
$ forall a. Bool -> Literal a
BooleanLiteral Bool
b
ReflectableOrdering Ordering
o -> SourceSpan -> Qualified (ProperName 'ConstructorName) -> Expr
Constructor SourceSpan
NullSourceSpan forall a b. (a -> b) -> a -> b
$ case Ordering
o of
Ordering
LT -> Qualified (ProperName 'ConstructorName)
C.C_LT
Ordering
EQ -> Qualified (ProperName 'ConstructorName)
C.C_EQ
Ordering
GT -> Qualified (ProperName 'ConstructorName)
C.C_GT
namedInstanceIdentifier :: Evidence -> Maybe (Qualified Ident)
namedInstanceIdentifier :: Evidence -> Maybe (Qualified Ident)
namedInstanceIdentifier (NamedInstance Qualified Ident
i) = forall a. a -> Maybe a
Just Qualified Ident
i
namedInstanceIdentifier Evidence
_ = forall a. Maybe a
Nothing
type TypeClassDict = TypeClassDictionaryInScope Evidence
type InstanceContext = M.Map QualifiedBy
(M.Map (Qualified (ProperName 'ClassName))
(M.Map (Qualified Ident) (NonEmpty NamedDict)))
findDicts :: InstanceContext -> Qualified (ProperName 'ClassName) -> QualifiedBy -> [TypeClassDict]
findDicts :: InstanceContext
-> Qualified (ProperName 'ClassName)
-> QualifiedBy
-> [TypeClassDict]
findDicts InstanceContext
ctx Qualified (ProperName 'ClassName)
cn = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Qualified Ident -> Evidence
NamedInstance) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. NonEmpty a -> [a]
NEL.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall k a. Map k a -> [a]
M.elems forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Qualified (ProperName 'ClassName)
cn forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall a b c. (a -> b -> c) -> b -> a -> c
flip forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup InstanceContext
ctx)
type Matching a = M.Map Text a
combineContexts :: InstanceContext -> InstanceContext -> InstanceContext
combineContexts :: InstanceContext -> InstanceContext -> InstanceContext
combineContexts = forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith (forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith (forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith forall a. Semigroup a => a -> a -> a
(<>)))
replaceTypeClassDictionaries
:: forall m
. (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m, MonadSupply m)
=> Bool
-> Expr
-> m (Expr, [(Ident, InstanceContext, SourceConstraint)])
replaceTypeClassDictionaries :: forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
MonadWriter MultipleErrors m, MonadSupply m) =>
Bool
-> Expr -> m (Expr, [(Ident, InstanceContext, SourceConstraint)])
replaceTypeClassDictionaries Bool
shouldGeneralize Expr
expr = 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
M.empty forall a b. (a -> b) -> a -> b
$ do
let loop :: Expr -> StateT InstanceContext m Expr
loop Expr
e = do
(Expr
e', Any
solved) <- Expr -> StateT InstanceContext m (Expr, Any)
deferPass Expr
e
if Any -> Bool
getAny Any
solved
then Expr -> StateT InstanceContext m Expr
loop Expr
e'
else forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e'
Expr -> StateT InstanceContext m Expr
loop Expr
expr forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Expr
-> StateT
InstanceContext
m
(Expr, [(Ident, InstanceContext, SourceConstraint)])
generalizePass
where
deferPass :: Expr -> StateT InstanceContext m (Expr, Any)
deferPass :: Expr -> StateT InstanceContext m (Expr, Any)
deferPass = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall a b. (a, b) -> a
fst) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr
-> WriterT
(Any, [(Ident, InstanceContext, SourceConstraint)])
(StateT InstanceContext m)
Expr
f where
f :: Expr -> WriterT (Any, [(Ident, InstanceContext, SourceConstraint)]) (StateT InstanceContext m) Expr
(Declaration
-> WriterT
(Any, [(Ident, InstanceContext, SourceConstraint)])
(StateT InstanceContext m)
Declaration
_, Expr
-> WriterT
(Any, [(Ident, InstanceContext, SourceConstraint)])
(StateT InstanceContext m)
Expr
f, Binder
-> WriterT
(Any, [(Ident, InstanceContext, SourceConstraint)])
(StateT InstanceContext m)
Binder
_) = forall (m :: * -> *).
Monad m =>
(Declaration -> m Declaration)
-> (Expr -> m Expr)
-> (Binder -> m Binder)
-> (Declaration -> m Declaration, Expr -> m Expr,
Binder -> m Binder)
everywhereOnValuesTopDownM forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
-> Expr
-> WriterT
(Any, [(Ident, InstanceContext, SourceConstraint)])
(StateT InstanceContext m)
Expr
go Bool
True) forall (m :: * -> *) a. Monad m => a -> m a
return
generalizePass :: Expr -> StateT InstanceContext m (Expr, [(Ident, InstanceContext, SourceConstraint)])
generalizePass :: Expr
-> StateT
InstanceContext
m
(Expr, [(Ident, InstanceContext, SourceConstraint)])
generalizePass = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall a b. (a, b) -> b
snd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr
-> WriterT
(Any, [(Ident, InstanceContext, SourceConstraint)])
(StateT InstanceContext m)
Expr
f where
f :: Expr -> WriterT (Any, [(Ident, InstanceContext, SourceConstraint)]) (StateT InstanceContext m) Expr
(Declaration
-> WriterT
(Any, [(Ident, InstanceContext, SourceConstraint)])
(StateT InstanceContext m)
Declaration
_, Expr
-> WriterT
(Any, [(Ident, InstanceContext, SourceConstraint)])
(StateT InstanceContext m)
Expr
f, Binder
-> WriterT
(Any, [(Ident, InstanceContext, SourceConstraint)])
(StateT InstanceContext m)
Binder
_) = forall (m :: * -> *).
Monad m =>
(Declaration -> m Declaration)
-> (Expr -> m Expr)
-> (Binder -> m Binder)
-> (Declaration -> m Declaration, Expr -> m Expr,
Binder -> m Binder)
everywhereOnValuesTopDownM forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
-> Expr
-> WriterT
(Any, [(Ident, InstanceContext, SourceConstraint)])
(StateT InstanceContext m)
Expr
go Bool
False) forall (m :: * -> *) a. Monad m => a -> m a
return
go :: Bool -> Expr -> WriterT (Any, [(Ident, InstanceContext, SourceConstraint)]) (StateT InstanceContext m) Expr
go :: Bool
-> Expr
-> WriterT
(Any, [(Ident, InstanceContext, SourceConstraint)])
(StateT InstanceContext m)
Expr
go Bool
deferErrors (TypeClassDictionary SourceConstraint
constraint InstanceContext
context [ErrorMessageHint]
hints) =
forall e (m :: * -> *) a. MonadError e m => (e -> e) -> m a -> m a
rethrow ([ErrorMessageHint] -> MultipleErrors -> MultipleErrors
addHints [ErrorMessageHint]
hints) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
MonadWriter MultipleErrors m, MonadSupply m) =>
SolverOptions
-> SourceConstraint
-> InstanceContext
-> [ErrorMessageHint]
-> WriterT
(Any, [(Ident, InstanceContext, SourceConstraint)])
(StateT InstanceContext m)
Expr
entails (Bool -> Bool -> SolverOptions
SolverOptions Bool
shouldGeneralize Bool
deferErrors) SourceConstraint
constraint InstanceContext
context [ErrorMessageHint]
hints
go Bool
_ Expr
other = forall (m :: * -> *) a. Monad m => a -> m a
return Expr
other
data EntailsResult a
= Solved a TypeClassDict
| Unsolved SourceConstraint
| Deferred
deriving Int -> EntailsResult a -> ShowS
forall a. Show a => Int -> EntailsResult a -> ShowS
forall a. Show a => [EntailsResult a] -> ShowS
forall a. Show a => EntailsResult a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [EntailsResult a] -> ShowS
$cshowList :: forall a. Show a => [EntailsResult a] -> ShowS
show :: EntailsResult a -> String
$cshow :: forall a. Show a => EntailsResult a -> String
showsPrec :: Int -> EntailsResult a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> EntailsResult a -> ShowS
Show
data SolverOptions = SolverOptions
{ SolverOptions -> Bool
solverShouldGeneralize :: Bool
, SolverOptions -> Bool
solverDeferErrors :: Bool
}
data Matched t
= Match t
| Apart
| Unknown
deriving (Matched t -> Matched t -> Bool
forall t. Eq t => Matched t -> Matched t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Matched t -> Matched t -> Bool
$c/= :: forall t. Eq t => Matched t -> Matched t -> Bool
== :: Matched t -> Matched t -> Bool
$c== :: forall t. Eq t => Matched t -> Matched t -> Bool
Eq, Int -> Matched t -> ShowS
forall t. Show t => Int -> Matched t -> ShowS
forall t. Show t => [Matched t] -> ShowS
forall t. Show t => Matched t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Matched t] -> ShowS
$cshowList :: forall t. Show t => [Matched t] -> ShowS
show :: Matched t -> String
$cshow :: forall t. Show t => Matched t -> String
showsPrec :: Int -> Matched t -> ShowS
$cshowsPrec :: forall t. Show t => Int -> Matched t -> ShowS
Show, forall a b. a -> Matched b -> Matched a
forall a b. (a -> b) -> Matched a -> Matched b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Matched b -> Matched a
$c<$ :: forall a b. a -> Matched b -> Matched a
fmap :: forall a b. (a -> b) -> Matched a -> Matched b
$cfmap :: forall a b. (a -> b) -> Matched a -> Matched b
Functor)
instance Semigroup t => Semigroup (Matched t) where
(Match t
l) <> :: Matched t -> Matched t -> Matched t
<> (Match t
r) = forall t. t -> Matched t
Match (t
l forall a. Semigroup a => a -> a -> a
<> t
r)
Matched t
Apart <> Matched t
_ = forall t. Matched t
Apart
Matched t
_ <> Matched t
Apart = forall t. Matched t
Apart
Matched t
_ <> Matched t
_ = forall t. Matched t
Unknown
instance Monoid t => Monoid (Matched t) where
mempty :: Matched t
mempty = forall t. t -> Matched t
Match forall a. Monoid a => a
mempty
entails
:: forall m
. (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m, MonadSupply m)
=> SolverOptions
-> SourceConstraint
-> InstanceContext
-> [ErrorMessageHint]
-> WriterT (Any, [(Ident, InstanceContext, SourceConstraint)]) (StateT InstanceContext m) Expr
entails :: forall (m :: * -> *).
(MonadState CheckState m, MonadError MultipleErrors m,
MonadWriter MultipleErrors m, MonadSupply m) =>
SolverOptions
-> SourceConstraint
-> InstanceContext
-> [ErrorMessageHint]
-> WriterT
(Any, [(Ident, InstanceContext, SourceConstraint)])
(StateT InstanceContext m)
Expr
entails SolverOptions{Bool
solverDeferErrors :: Bool
solverShouldGeneralize :: Bool
solverDeferErrors :: SolverOptions -> Bool
solverShouldGeneralize :: SolverOptions -> Bool
..} SourceConstraint
constraint InstanceContext
context [ErrorMessageHint]
hints =
forall (f :: * -> *) a.
Applicative f =>
([Type a] -> f [Type a]) -> Constraint a -> f (Constraint a)
overConstraintArgsAll (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall e (m :: * -> *).
(e ~ MultipleErrors, MonadState CheckState m, MonadError e m) =>
SourceType -> m SourceType
replaceAllTypeSynonyms) SourceConstraint
constraint forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SourceConstraint
-> WriterT
(Any, [(Ident, InstanceContext, SourceConstraint)])
(StateT InstanceContext m)
Expr
solve
where
forClassNameM :: Environment -> InstanceContext -> Qualified (ProperName 'ClassName) -> [SourceType] -> [SourceType] -> m [TypeClassDict]
forClassNameM :: Environment
-> InstanceContext
-> Qualified (ProperName 'ClassName)
-> [SourceType]
-> [SourceType]
-> m [TypeClassDict]
forClassNameM Environment
env InstanceContext
ctx cn :: Qualified (ProperName 'ClassName)
cn@Qualified (ProperName 'ClassName)
C.Coercible [SourceType]
kinds [SourceType]
args =
forall a. a -> Maybe a -> a
fromMaybe (Environment
-> InstanceContext
-> Qualified (ProperName 'ClassName)
-> [SourceType]
-> [SourceType]
-> [TypeClassDict]
forClassName Environment
env InstanceContext
ctx Qualified (ProperName 'ClassName)
cn [SourceType]
kinds [SourceType]
args) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
Environment
-> InstanceContext
-> [SourceType]
-> [SourceType]
-> m (Maybe [TypeClassDict])
solveCoercible Environment
env InstanceContext
ctx [SourceType]
kinds [SourceType]
args
forClassNameM Environment
env InstanceContext
ctx Qualified (ProperName 'ClassName)
cn [SourceType]
kinds [SourceType]
args =
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Environment
-> InstanceContext
-> Qualified (ProperName 'ClassName)
-> [SourceType]
-> [SourceType]
-> [TypeClassDict]
forClassName Environment
env InstanceContext
ctx Qualified (ProperName 'ClassName)
cn [SourceType]
kinds [SourceType]
args
forClassName :: Environment -> InstanceContext -> Qualified (ProperName 'ClassName) -> [SourceType] -> [SourceType] -> [TypeClassDict]
forClassName :: Environment
-> InstanceContext
-> Qualified (ProperName 'ClassName)
-> [SourceType]
-> [SourceType]
-> [TypeClassDict]
forClassName Environment
_ InstanceContext
ctx cn :: Qualified (ProperName 'ClassName)
cn@Qualified (ProperName 'ClassName)
C.Warn [SourceType]
_ [SourceType
msg] =
InstanceContext
-> Qualified (ProperName 'ClassName)
-> QualifiedBy
-> [TypeClassDict]
findDicts InstanceContext
ctx Qualified (ProperName 'ClassName)
cn QualifiedBy
ByNullSourcePos forall a. [a] -> [a] -> [a]
++ [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 (SourceType -> Evidence
WarnInstance SourceType
msg) [] Qualified (ProperName 'ClassName)
C.Warn [] [] [SourceType
msg] forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.IsSymbol [SourceType]
_ [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> Maybe [TypeClassDict]
solveIsSymbol [SourceType]
args = [TypeClassDict]
dicts
forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.SymbolCompare [SourceType]
_ [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> Maybe [TypeClassDict]
solveSymbolCompare [SourceType]
args = [TypeClassDict]
dicts
forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.SymbolAppend [SourceType]
_ [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> Maybe [TypeClassDict]
solveSymbolAppend [SourceType]
args = [TypeClassDict]
dicts
forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.SymbolCons [SourceType]
_ [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> Maybe [TypeClassDict]
solveSymbolCons [SourceType]
args = [TypeClassDict]
dicts
forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.IntAdd [SourceType]
_ [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> Maybe [TypeClassDict]
solveIntAdd [SourceType]
args = [TypeClassDict]
dicts
forClassName Environment
_ InstanceContext
ctx Qualified (ProperName 'ClassName)
C.IntCompare [SourceType]
_ [SourceType]
args | Just [TypeClassDict]
dicts <- InstanceContext -> [SourceType] -> Maybe [TypeClassDict]
solveIntCompare InstanceContext
ctx [SourceType]
args = [TypeClassDict]
dicts
forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.IntMul [SourceType]
_ [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> Maybe [TypeClassDict]
solveIntMul [SourceType]
args = [TypeClassDict]
dicts
forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.IntToString [SourceType]
_ [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> Maybe [TypeClassDict]
solveIntToString [SourceType]
args = [TypeClassDict]
dicts
forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.Reflectable [SourceType]
_ [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> Maybe [TypeClassDict]
solveReflectable [SourceType]
args = [TypeClassDict]
dicts
forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.RowUnion [SourceType]
kinds [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
solveUnion [SourceType]
kinds [SourceType]
args = [TypeClassDict]
dicts
forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.RowNub [SourceType]
kinds [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
solveNub [SourceType]
kinds [SourceType]
args = [TypeClassDict]
dicts
forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.RowLacks [SourceType]
kinds [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
solveLacks [SourceType]
kinds [SourceType]
args = [TypeClassDict]
dicts
forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.RowCons [SourceType]
kinds [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
solveRowCons [SourceType]
kinds [SourceType]
args = [TypeClassDict]
dicts
forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.RowToList [SourceType]
kinds [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
solveRowToList [SourceType]
kinds [SourceType]
args = [TypeClassDict]
dicts
forClassName Environment
_ InstanceContext
ctx cn :: Qualified (ProperName 'ClassName)
cn@(Qualified (ByModuleName ModuleName
mn) ProperName 'ClassName
_) [SourceType]
_ [SourceType]
tys = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (InstanceContext
-> Qualified (ProperName 'ClassName)
-> QualifiedBy
-> [TypeClassDict]
findDicts InstanceContext
ctx Qualified (ProperName 'ClassName)
cn) (forall a. Ord a => [a] -> [a]
ordNub (QualifiedBy
ByNullSourcePos forall a. a -> [a] -> [a]
: ModuleName -> QualifiedBy
ByModuleName ModuleName
mn forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map ModuleName -> QualifiedBy
ByModuleName (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe SourceType -> Maybe ModuleName
ctorModules [SourceType]
tys)))
forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
_ [SourceType]
_ [SourceType]
_ = forall a. HasCallStack => String -> a
internalError String
"forClassName: expected qualified class name"
ctorModules :: SourceType -> Maybe ModuleName
ctorModules :: SourceType -> Maybe ModuleName
ctorModules (TypeConstructor (SourceSpan, [Comment])
_ (Qualified (ByModuleName ModuleName
mn) ProperName 'TypeName
_)) = forall a. a -> Maybe a
Just ModuleName
mn
ctorModules (TypeConstructor (SourceSpan, [Comment])
_ (Qualified (BySourcePos SourcePos
_) ProperName 'TypeName
_)) = forall a. HasCallStack => String -> a
internalError String
"ctorModules: unqualified type name"
ctorModules (TypeApp (SourceSpan, [Comment])
_ SourceType
ty SourceType
_) = SourceType -> Maybe ModuleName
ctorModules SourceType
ty
ctorModules (KindApp (SourceSpan, [Comment])
_ SourceType
ty SourceType
_) = SourceType -> Maybe ModuleName
ctorModules SourceType
ty
ctorModules (KindedType (SourceSpan, [Comment])
_ SourceType
ty SourceType
_) = SourceType -> Maybe ModuleName
ctorModules SourceType
ty
ctorModules SourceType
_ = forall a. Maybe a
Nothing
valUndefined :: Expr
valUndefined :: Expr
valUndefined = SourceSpan -> Qualified Ident -> Expr
Var SourceSpan
nullSourceSpan Qualified Ident
C.I_undefined
solve :: SourceConstraint -> WriterT (Any, [(Ident, InstanceContext, SourceConstraint)]) (StateT InstanceContext m) Expr
solve :: SourceConstraint
-> WriterT
(Any, [(Ident, InstanceContext, SourceConstraint)])
(StateT InstanceContext m)
Expr
solve = Int
-> [ErrorMessageHint]
-> SourceConstraint
-> WriterT
(Any, [(Ident, InstanceContext, SourceConstraint)])
(StateT InstanceContext m)
Expr
go Int
0 [ErrorMessageHint]
hints
where
go :: Int -> [ErrorMessageHint] -> SourceConstraint -> WriterT (Any, [(Ident, InstanceContext, SourceConstraint)]) (StateT InstanceContext m) Expr
go :: Int
-> [ErrorMessageHint]
-> SourceConstraint
-> WriterT
(Any, [(Ident, InstanceContext, SourceConstraint)])
(StateT InstanceContext m)
Expr
go Int
work [ErrorMessageHint]
_ (Constraint (SourceSpan, [Comment])
_ Qualified (ProperName 'ClassName)
className' [SourceType]
_ [SourceType]
tys' Maybe ConstraintData
_) | Int
work forall a. Ord a => a -> a -> Bool
> Int
1000 = 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 a b. (a -> b) -> a -> b
$ Qualified (ProperName 'ClassName)
-> [SourceType] -> SimpleErrorMessage
PossiblyInfiniteInstance Qualified (ProperName 'ClassName)
className' [SourceType]
tys'
go Int
work [ErrorMessageHint]
hints' con :: SourceConstraint
con@(Constraint (SourceSpan, [Comment])
_ Qualified (ProperName 'ClassName)
className' [SourceType]
kinds' [SourceType]
tys' Maybe ConstraintData
conInfo) = forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m) =>
ErrorMessageHint -> m a -> m a
withErrorMessageHint (SourceConstraint -> ErrorMessageHint
ErrorSolvingConstraint SourceConstraint
con) forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT forall a b. (a -> b) -> a -> b
$ do
Substitution
latestSubst <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Substitution
checkSubstitution
let kinds'' :: [SourceType]
kinds'' = forall a b. (a -> b) -> [a] -> [b]
map (Substitution -> SourceType -> SourceType
substituteType Substitution
latestSubst) [SourceType]
kinds'
tys'' :: [SourceType]
tys'' = forall a b. (a -> b) -> [a] -> [b]
map (Substitution -> SourceType -> SourceType
substituteType Substitution
latestSubst) [SourceType]
tys'
InstanceContext
inferred <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall s (m :: * -> *). MonadState s m => m s
get
Environment
env <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Environment
checkEnv
let classesInScope :: Map (Qualified (ProperName 'ClassName)) TypeClassData
classesInScope = Environment
-> Map (Qualified (ProperName 'ClassName)) TypeClassData
typeClasses Environment
env
TypeClassData
{ [FunctionalDependency]
typeClassDependencies :: TypeClassData -> [FunctionalDependency]
typeClassDependencies :: [FunctionalDependency]
typeClassDependencies
, Bool
typeClassIsEmpty :: TypeClassData -> Bool
typeClassIsEmpty :: Bool
typeClassIsEmpty
, Set (Set Int)
typeClassCoveringSets :: TypeClassData -> Set (Set Int)
typeClassCoveringSets :: Set (Set Int)
typeClassCoveringSets
} <- case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Qualified (ProperName 'ClassName)
className' Map (Qualified (ProperName 'ClassName)) TypeClassData
classesInScope of
Maybe TypeClassData
Nothing -> 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 a b. (a -> b) -> a -> b
$ Qualified (ProperName 'ClassName) -> SimpleErrorMessage
UnknownClass Qualified (ProperName 'ClassName)
className'
Just TypeClassData
tcd -> forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeClassData
tcd
[TypeClassDict]
dicts <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Environment
-> InstanceContext
-> Qualified (ProperName 'ClassName)
-> [SourceType]
-> [SourceType]
-> m [TypeClassDict]
forClassNameM Environment
env (InstanceContext -> InstanceContext -> InstanceContext
combineContexts InstanceContext
context InstanceContext
inferred) Qualified (ProperName 'ClassName)
className' [SourceType]
kinds'' [SourceType]
tys''
let (forall a. [Maybe a] -> [a]
catMaybes -> [Qualified (Either SourceType Ident)]
ambiguous, [(Matching [SourceType], TypeClassDict)]
instances) = forall a b. [Either a b] -> ([a], [b])
partitionEithers forall a b. (a -> b) -> a -> b
$ do
NonEmpty TypeClassDict
chain :: NonEmpty TypeClassDict <-
forall (f :: * -> *) a.
Foldable f =>
(a -> a -> Bool) -> f a -> [NonEmpty a]
NEL.groupBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall v. TypeClassDictionaryInScope v -> Maybe ChainId
tcdChain) forall a b. (a -> b) -> a -> b
$
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (forall v. TypeClassDictionaryInScope v -> Maybe ChainId
tcdChain forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& forall v. TypeClassDictionaryInScope v -> Integer
tcdIndex)
[TypeClassDict]
dicts
let found :: Either
(Either
(Maybe (Qualified (Either SourceType Ident)))
(Matching [SourceType], TypeClassDict))
(NonEmpty ())
found = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for (forall a. NonEmpty a -> NonEmpty (NonEmpty a)
tails1 NonEmpty TypeClassDict
chain) forall a b. (a -> b) -> a -> b
$ \(TypeClassDict
tcd :| [TypeClassDict]
tl) ->
case [FunctionalDependency]
-> TypeClassDict -> [SourceType] -> Matched (Matching [SourceType])
matches [FunctionalDependency]
typeClassDependencies TypeClassDict
tcd [SourceType]
tys'' of
Matched (Matching [SourceType])
Apart -> forall a b. b -> Either a b
Right ()
Match Matching [SourceType]
substs -> forall a b. a -> Either a b
Left (forall a b. b -> Either a b
Right (Matching [SourceType]
substs, TypeClassDict
tcd))
Matched (Matching [SourceType])
Unknown ->
if forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall v. TypeClassDictionaryInScope v -> Maybe ChainId
tcdChain TypeClassDict
tcd) Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeClassDict]
tl
then forall a b. b -> Either a b
Right ()
else forall a b. a -> Either a b
Left (forall a b. a -> Either a b
Left (TypeClassDict -> Maybe (Qualified (Either SourceType Ident))
tcdToInstanceDescription TypeClassDict
tcd))
forall a b. [Either a b] -> [a]
lefts [Either
(Either
(Maybe (Qualified (Either SourceType Ident)))
(Matching [SourceType], TypeClassDict))
(NonEmpty ())
found]
EntailsResult (Matching [SourceType])
solution <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a.
[SourceType]
-> [SourceType]
-> [Qualified (Either SourceType Ident)]
-> [(a, TypeClassDict)]
-> Bool
-> m (EntailsResult a)
unique [SourceType]
kinds'' [SourceType]
tys'' [Qualified (Either SourceType Ident)]
ambiguous [(Matching [SourceType], TypeClassDict)]
instances ([SourceType] -> Set (Set Int) -> Bool
unknownsInAllCoveringSets [SourceType]
tys'' Set (Set Int)
typeClassCoveringSets)
case EntailsResult (Matching [SourceType])
solution of
Solved Matching [SourceType]
substs TypeClassDict
tcd -> do
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Bool -> Any
Any Bool
True, forall a. Monoid a => a
mempty)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ Matching [SourceType]
substs forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
Applicative m =>
(a -> a -> m ()) -> [a] -> m ()
pairwiseM forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes
let subst :: Map Text SourceType
subst = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. [a] -> a
head Matching [SourceType]
substs
Substitution
currentSubst <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Substitution
checkSubstitution
Map Text SourceType
subst' <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ TypeClassDict -> Map Text SourceType -> m (Map Text SourceType)
withFreshTypes TypeClassDict
tcd (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Substitution -> SourceType -> SourceType
substituteType Substitution
currentSubst) Map Text SourceType
subst)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (\SourceType
t1 SourceType
t2 -> do
let inferredType :: SourceType
inferredType = forall a. [(Text, Type a)] -> Type a -> Type a
replaceAllTypeVars (forall k a. Map k a -> [(k, a)]
M.toList Map Text SourceType
subst') SourceType
t1
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
SourceType -> SourceType -> m ()
unifyTypes SourceType
inferredType SourceType
t2) (forall v. TypeClassDictionaryInScope v -> [SourceType]
tcdInstanceTypes TypeClassDict
tcd) [SourceType]
tys''
Substitution
currentSubst' <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Substitution
checkSubstitution
let subst'' :: Map Text SourceType
subst'' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Substitution -> SourceType -> SourceType
substituteType Substitution
currentSubst') Map Text SourceType
subst'
Maybe [Expr]
args <- Map Text SourceType
-> ErrorMessageHint
-> Maybe [SourceConstraint]
-> WriterT
(Any, [(Ident, InstanceContext, SourceConstraint)])
(StateT InstanceContext m)
(Maybe [Expr])
solveSubgoals Map Text SourceType
subst'' (SourceConstraint -> ErrorMessageHint
ErrorSolvingConstraint SourceConstraint
con) (forall v. TypeClassDictionaryInScope v -> Maybe [SourceConstraint]
tcdDependencies TypeClassDict
tcd)
Expr
initDict <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Evidence -> Maybe [Expr] -> m Expr
mkDictionary (forall v. TypeClassDictionaryInScope v -> v
tcdValue TypeClassDict
tcd) Maybe [Expr]
args
let match :: Expr
match = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Qualified (ProperName 'ClassName)
className, Integer
index) Expr
dict -> Expr -> Qualified (ProperName 'ClassName) -> Integer -> Expr
subclassDictionaryValue Expr
dict Qualified (ProperName 'ClassName)
className Integer
index)
Expr
initDict
(forall v.
TypeClassDictionaryInScope v
-> [(Qualified (ProperName 'ClassName), Integer)]
tcdPath TypeClassDict
tcd)
forall (m :: * -> *) a. Monad m => a -> m a
return (if Bool
typeClassIsEmpty then Expr -> Expr
Unused Expr
match else Expr
match)
Unsolved SourceConstraint
unsolved -> do
Ident
ident <- forall (m :: * -> *). MonadSupply m => Text -> m Ident
freshIdent (Text
"dict" forall a. Semigroup a => a -> a -> a
<> forall (a :: ProperNameType). ProperName a -> Text
runProperName (forall a. Qualified a -> a
disqualify (forall a. Constraint a -> Qualified (ProperName 'ClassName)
constraintClass SourceConstraint
unsolved)))
let qident :: Qualified Ident
qident = forall a. QualifiedBy -> a -> Qualified a
Qualified QualifiedBy
ByNullSourcePos Ident
ident
[NamedDict]
newDicts <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadState CheckState m =>
[(Qualified (ProperName 'ClassName), Integer)]
-> Qualified Ident -> SourceConstraint -> m [NamedDict]
newDictionaries [] Qualified Ident
qident SourceConstraint
unsolved
let newContext :: InstanceContext
newContext = [NamedDict] -> InstanceContext
mkContext [NamedDict]
newDicts
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (InstanceContext -> InstanceContext -> InstanceContext
combineContexts InstanceContext
newContext)
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (forall a. Monoid a => a
mempty, [(Ident
ident, InstanceContext
context, SourceConstraint
unsolved)])
forall (m :: * -> *) a. Monad m => a -> m a
return (SourceSpan -> Qualified Ident -> Expr
Var SourceSpan
nullSourceSpan Qualified Ident
qident)
EntailsResult (Matching [SourceType])
Deferred ->
forall (m :: * -> *) a. Monad m => a -> m a
return (SourceConstraint -> InstanceContext -> [ErrorMessageHint] -> Expr
TypeClassDictionary (Qualified (ProperName 'ClassName)
-> [SourceType]
-> [SourceType]
-> Maybe ConstraintData
-> SourceConstraint
srcConstraint Qualified (ProperName 'ClassName)
className' [SourceType]
kinds'' [SourceType]
tys'' Maybe ConstraintData
conInfo) InstanceContext
context [ErrorMessageHint]
hints')
where
withFreshTypes
:: TypeClassDict
-> Matching SourceType
-> m (Matching SourceType)
withFreshTypes :: TypeClassDict -> Map Text SourceType -> m (Map Text SourceType)
withFreshTypes TypeClassDictionaryInScope{Integer
[(Text, SourceType)]
[(Qualified (ProperName 'ClassName), Integer)]
[SourceType]
Maybe [SourceConstraint]
Maybe ChainId
Maybe SourceType
Qualified (ProperName 'ClassName)
Evidence
tcdDescription :: forall v. TypeClassDictionaryInScope v -> Maybe SourceType
tcdInstanceKinds :: forall v. TypeClassDictionaryInScope v -> [SourceType]
tcdForAll :: forall v. TypeClassDictionaryInScope v -> [(Text, SourceType)]
tcdClassName :: forall v.
TypeClassDictionaryInScope v -> Qualified (ProperName 'ClassName)
tcdDescription :: Maybe SourceType
tcdDependencies :: Maybe [SourceConstraint]
tcdInstanceTypes :: [SourceType]
tcdInstanceKinds :: [SourceType]
tcdForAll :: [(Text, SourceType)]
tcdClassName :: Qualified (ProperName 'ClassName)
tcdPath :: [(Qualified (ProperName 'ClassName), Integer)]
tcdValue :: Evidence
tcdIndex :: Integer
tcdChain :: Maybe ChainId
tcdPath :: forall v.
TypeClassDictionaryInScope v
-> [(Qualified (ProperName 'ClassName), Integer)]
tcdValue :: forall v. TypeClassDictionaryInScope v -> v
tcdDependencies :: forall v. TypeClassDictionaryInScope v -> Maybe [SourceConstraint]
tcdInstanceTypes :: forall v. TypeClassDictionaryInScope v -> [SourceType]
tcdIndex :: forall v. TypeClassDictionaryInScope v -> Integer
tcdChain :: forall v. TypeClassDictionaryInScope v -> Maybe ChainId
..} Map Text SourceType
initSubst = do
Map Text SourceType
subst <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM forall {m :: * -> *}.
MonadState CheckState m =>
Map Text SourceType
-> (Text, SourceType) -> m (Map Text SourceType)
withFreshType Map Text SourceType
initSubst forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall k a. Ord k => k -> Map k a -> Bool
M.notMember Map Text SourceType
initSubst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Text, SourceType)]
tcdForAll
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ (forall k a. Map k a -> [(k, a)]
M.toList Map Text SourceType
initSubst) forall a b. (a -> b) -> a -> b
$ Map Text SourceType -> (Text, SourceType) -> m ()
unifySubstKind Map Text SourceType
subst
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map Text SourceType
subst
where
withFreshType :: Map Text SourceType
-> (Text, SourceType) -> m (Map Text SourceType)
withFreshType Map Text SourceType
subst (Text
var, SourceType
kind) = do
SourceType
ty <- forall (m :: * -> *).
MonadState CheckState m =>
SourceType -> m SourceType
freshTypeWithKind forall a b. (a -> b) -> a -> b
$ forall a. [(Text, Type a)] -> Type a -> Type a
replaceAllTypeVars (forall k a. Map k a -> [(k, a)]
M.toList Map Text SourceType
subst) SourceType
kind
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Text
var SourceType
ty Map Text SourceType
subst
unifySubstKind :: Map Text SourceType -> (Text, SourceType) -> m ()
unifySubstKind Map Text SourceType
subst (Text
var, SourceType
ty) =
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ (forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Text
var [(Text, SourceType)]
tcdForAll) forall a b. (a -> b) -> a -> b
$ \SourceType
instKind -> do
SourceType
tyKind <- forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> m SourceType
elaborateKind SourceType
ty
Substitution
currentSubst <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Substitution
checkSubstitution
forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m,
HasCallStack) =>
SourceType -> SourceType -> m ()
unifyKinds'
(Substitution -> SourceType -> SourceType
substituteType Substitution
currentSubst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [(Text, Type a)] -> Type a -> Type a
replaceAllTypeVars (forall k a. Map k a -> [(k, a)]
M.toList Map Text SourceType
subst) forall a b. (a -> b) -> a -> b
$ SourceType
instKind)
(Substitution -> SourceType -> SourceType
substituteType Substitution
currentSubst SourceType
tyKind)
unique :: [SourceType] -> [SourceType] -> [Qualified (Either SourceType Ident)] -> [(a, TypeClassDict)] -> Bool -> m (EntailsResult a)
unique :: forall a.
[SourceType]
-> [SourceType]
-> [Qualified (Either SourceType Ident)]
-> [(a, TypeClassDict)]
-> Bool
-> m (EntailsResult a)
unique [SourceType]
kindArgs [SourceType]
tyArgs [Qualified (Either SourceType Ident)]
ambiguous [] Bool
unks
| Bool
solverDeferErrors = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. EntailsResult a
Deferred
| Bool
solverShouldGeneralize Bool -> Bool -> Bool
&& ((forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SourceType]
kindArgs Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SourceType]
tyArgs) Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. Type a -> Bool
canBeGeneralized [SourceType]
kindArgs Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. Type a -> Bool
canBeGeneralized [SourceType]
tyArgs) =
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. SourceConstraint -> EntailsResult a
Unsolved (Qualified (ProperName 'ClassName)
-> [SourceType]
-> [SourceType]
-> Maybe ConstraintData
-> SourceConstraint
srcConstraint Qualified (ProperName 'ClassName)
className' [SourceType]
kindArgs [SourceType]
tyArgs Maybe ConstraintData
conInfo))
| Bool
otherwise = 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 a b. (a -> b) -> a -> b
$ SourceConstraint
-> [Qualified (Either SourceType Ident)]
-> Bool
-> SimpleErrorMessage
NoInstanceFound (Qualified (ProperName 'ClassName)
-> [SourceType]
-> [SourceType]
-> Maybe ConstraintData
-> SourceConstraint
srcConstraint Qualified (ProperName 'ClassName)
className' [SourceType]
kindArgs [SourceType]
tyArgs Maybe ConstraintData
conInfo) [Qualified (Either SourceType Ident)]
ambiguous Bool
unks
unique [SourceType]
_ [SourceType]
_ [Qualified (Either SourceType Ident)]
_ [(a
a, TypeClassDict
dict)] Bool
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> TypeClassDict -> EntailsResult a
Solved a
a TypeClassDict
dict
unique [SourceType]
_ [SourceType]
tyArgs [Qualified (Either SourceType Ident)]
_ [(a, TypeClassDict)]
tcds Bool
_
| forall a. (a -> a -> Bool) -> [a] -> Bool
pairwiseAny TypeClassDict -> TypeClassDict -> Bool
overlapping (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(a, TypeClassDict)]
tcds) =
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 a b. (a -> b) -> a -> b
$ Qualified (ProperName 'ClassName)
-> [SourceType]
-> [Qualified (Either SourceType Ident)]
-> SimpleErrorMessage
OverlappingInstances Qualified (ProperName 'ClassName)
className' [SourceType]
tyArgs ([(a, TypeClassDict)]
tcds forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeClassDict -> Maybe (Qualified (Either SourceType Ident))
tcdToInstanceDescription forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd))
| Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. a -> TypeClassDict -> EntailsResult a
Solved (forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
minimumBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v.
TypeClassDictionaryInScope v
-> [(Qualified (ProperName 'ClassName), Integer)]
tcdPath forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(a, TypeClassDict)]
tcds)
tcdToInstanceDescription :: TypeClassDict -> Maybe (Qualified (Either SourceType Ident))
tcdToInstanceDescription :: TypeClassDict -> Maybe (Qualified (Either SourceType Ident))
tcdToInstanceDescription TypeClassDictionaryInScope{ Maybe SourceType
tcdDescription :: Maybe SourceType
tcdDescription :: forall v. TypeClassDictionaryInScope v -> Maybe SourceType
tcdDescription, Evidence
tcdValue :: Evidence
tcdValue :: forall v. TypeClassDictionaryInScope v -> v
tcdValue } =
let nii :: Maybe (Qualified Ident)
nii = Evidence -> Maybe (Qualified Ident)
namedInstanceIdentifier Evidence
tcdValue
in case Maybe SourceType
tcdDescription of
Just SourceType
ty -> forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. QualifiedBy -> a -> Qualified a
Qualified (forall a b. a -> Either a b
Left SourceType
ty) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Maybe ModuleName -> QualifiedBy
byMaybeModuleName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Qualified a -> Maybe ModuleName
getQual) Maybe (Qualified Ident)
nii
Maybe SourceType
Nothing -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Qualified Ident)
nii
canBeGeneralized :: Type a -> Bool
canBeGeneralized :: forall a. Type a -> Bool
canBeGeneralized TUnknown{} = Bool
True
canBeGeneralized (KindedType a
_ Type a
t Type a
_) = forall a. Type a -> Bool
canBeGeneralized Type a
t
canBeGeneralized Type a
_ = Bool
False
overlapping :: TypeClassDict -> TypeClassDict -> Bool
overlapping :: TypeClassDict -> TypeClassDict -> Bool
overlapping TypeClassDictionaryInScope{ tcdPath :: forall v.
TypeClassDictionaryInScope v
-> [(Qualified (ProperName 'ClassName), Integer)]
tcdPath = (Qualified (ProperName 'ClassName), Integer)
_ : [(Qualified (ProperName 'ClassName), Integer)]
_ } TypeClassDict
_ = Bool
False
overlapping TypeClassDict
_ TypeClassDictionaryInScope{ tcdPath :: forall v.
TypeClassDictionaryInScope v
-> [(Qualified (ProperName 'ClassName), Integer)]
tcdPath = (Qualified (ProperName 'ClassName), Integer)
_ : [(Qualified (ProperName 'ClassName), Integer)]
_ } = Bool
False
overlapping TypeClassDictionaryInScope{ tcdDependencies :: forall v. TypeClassDictionaryInScope v -> Maybe [SourceConstraint]
tcdDependencies = Maybe [SourceConstraint]
Nothing } TypeClassDict
_ = Bool
False
overlapping TypeClassDict
_ TypeClassDictionaryInScope{ tcdDependencies :: forall v. TypeClassDictionaryInScope v -> Maybe [SourceConstraint]
tcdDependencies = Maybe [SourceConstraint]
Nothing } = Bool
False
overlapping TypeClassDict
tcd1 TypeClassDict
tcd2 = forall v. TypeClassDictionaryInScope v -> v
tcdValue TypeClassDict
tcd1 forall a. Eq a => a -> a -> Bool
/= forall v. TypeClassDictionaryInScope v -> v
tcdValue TypeClassDict
tcd2
solveSubgoals :: Matching SourceType -> ErrorMessageHint -> Maybe [SourceConstraint] -> WriterT (Any, [(Ident, InstanceContext, SourceConstraint)]) (StateT InstanceContext m) (Maybe [Expr])
solveSubgoals :: Map Text SourceType
-> ErrorMessageHint
-> Maybe [SourceConstraint]
-> WriterT
(Any, [(Ident, InstanceContext, SourceConstraint)])
(StateT InstanceContext m)
(Maybe [Expr])
solveSubgoals Map Text SourceType
_ ErrorMessageHint
_ Maybe [SourceConstraint]
Nothing = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
solveSubgoals Map Text SourceType
subst ErrorMessageHint
hint (Just [SourceConstraint]
subgoals) =
forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall e (m :: * -> *) a. MonadError e m => (e -> e) -> m a -> m a
rethrow (ErrorMessageHint -> MultipleErrors -> MultipleErrors
addHint ErrorMessageHint
hint) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int
-> [ErrorMessageHint]
-> SourceConstraint
-> WriterT
(Any, [(Ident, InstanceContext, SourceConstraint)])
(StateT InstanceContext m)
Expr
go (Int
work forall a. Num a => a -> a -> a
+ Int
1) ([ErrorMessageHint]
hints' forall a. Semigroup a => a -> a -> a
<> [ErrorMessageHint
hint]) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ([Type a] -> [Type a]) -> Constraint a -> Constraint a
mapConstraintArgsAll (forall a b. (a -> b) -> [a] -> [b]
map (forall a. [(Text, Type a)] -> Type a -> Type a
replaceAllTypeVars (forall k a. Map k a -> [(k, a)]
M.toList Map Text SourceType
subst)))) [SourceConstraint]
subgoals
useEmptyDict :: Maybe [Expr] -> Expr
useEmptyDict :: Maybe [Expr] -> Expr
useEmptyDict Maybe [Expr]
args = Expr -> Expr
Unused (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Expr -> Expr -> Expr
App forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binder -> Expr -> Expr
Abs (SourceSpan -> Ident -> Binder
VarBinder SourceSpan
nullSourceSpan Ident
UnusedIdent)) Expr
valUndefined (forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Maybe [Expr]
args))
mkDictionary :: Evidence -> Maybe [Expr] -> m Expr
mkDictionary :: Evidence -> Maybe [Expr] -> m Expr
mkDictionary (NamedInstance Qualified Ident
n) Maybe [Expr]
args = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Expr -> Expr
App (SourceSpan -> Qualified Ident -> Expr
Var SourceSpan
nullSourceSpan Qualified Ident
n) (forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Maybe [Expr]
args)
mkDictionary Evidence
EmptyClassInstance Maybe [Expr]
args = forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [Expr] -> Expr
useEmptyDict Maybe [Expr]
args)
mkDictionary (WarnInstance SourceType
msg) Maybe [Expr]
args = do
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleErrorMessage -> MultipleErrors
errorMessage forall a b. (a -> b) -> a -> b
$ SourceType -> SimpleErrorMessage
UserDefinedWarning SourceType
msg
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [Expr] -> Expr
useEmptyDict Maybe [Expr]
args)
mkDictionary (IsSymbolInstance PSString
sym) Maybe [Expr]
_ =
let fields :: [(PSString, Expr)]
fields = [ (PSString
"reflectSymbol", Binder -> Expr -> Expr
Abs (SourceSpan -> Ident -> Binder
VarBinder SourceSpan
nullSourceSpan Ident
UnusedIdent) (SourceSpan -> Literal Expr -> Expr
Literal SourceSpan
nullSourceSpan (forall a. PSString -> Literal a
StringLiteral PSString
sym))) ] in
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
App (SourceSpan -> Qualified (ProperName 'ConstructorName) -> Expr
Constructor SourceSpan
nullSourceSpan (forall (a :: ProperNameType) (b :: ProperNameType).
ProperName a -> ProperName b
coerceProperName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: ProperNameType). ProperName a -> ProperName a
dictTypeName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Qualified (ProperName 'ClassName)
C.IsSymbol)) (SourceSpan -> Literal Expr -> Expr
Literal SourceSpan
nullSourceSpan (forall a. [(PSString, a)] -> Literal a
ObjectLiteral [(PSString, Expr)]
fields))
mkDictionary (ReflectableInstance Reflectable
ref) Maybe [Expr]
_ =
let fields :: [(PSString, Expr)]
fields = [ (PSString
"reflectType", Binder -> Expr -> Expr
Abs (SourceSpan -> Ident -> Binder
VarBinder SourceSpan
nullSourceSpan Ident
UnusedIdent) (Reflectable -> Expr
asExpression Reflectable
ref)) ] in
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
App (SourceSpan -> Qualified (ProperName 'ConstructorName) -> Expr
Constructor SourceSpan
nullSourceSpan (forall (a :: ProperNameType) (b :: ProperNameType).
ProperName a -> ProperName b
coerceProperName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: ProperNameType). ProperName a -> ProperName a
dictTypeName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Qualified (ProperName 'ClassName)
C.Reflectable)) (SourceSpan -> Literal Expr -> Expr
Literal SourceSpan
nullSourceSpan (forall a. [(PSString, a)] -> Literal a
ObjectLiteral [(PSString, Expr)]
fields))
unknownsInAllCoveringSets :: [SourceType] -> S.Set (S.Set Int) -> Bool
unknownsInAllCoveringSets :: [SourceType] -> Set (Set Int) -> Bool
unknownsInAllCoveringSets [SourceType]
tyArgs = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Set Int
s -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Ord a => a -> Set a -> Bool
`S.member` Set Int
s) [Int]
unkIndices)
where unkIndices :: [Int]
unkIndices = forall a. (a -> Bool) -> [a] -> [Int]
findIndices forall a. Type a -> Bool
containsUnknowns [SourceType]
tyArgs
subclassDictionaryValue :: Expr -> Qualified (ProperName 'ClassName) -> Integer -> Expr
subclassDictionaryValue :: Expr -> Qualified (ProperName 'ClassName) -> Integer -> Expr
subclassDictionaryValue Expr
dict Qualified (ProperName 'ClassName)
className Integer
index =
Expr -> Expr -> Expr
App (PSString -> Expr -> Expr
Accessor (Text -> PSString
mkString (Qualified (ProperName 'ClassName) -> Integer -> Text
superclassName Qualified (ProperName 'ClassName)
className Integer
index)) Expr
dict) Expr
valUndefined
solveCoercible :: Environment -> InstanceContext -> [SourceType] -> [SourceType] -> m (Maybe [TypeClassDict])
solveCoercible :: Environment
-> InstanceContext
-> [SourceType]
-> [SourceType]
-> m (Maybe [TypeClassDict])
solveCoercible Environment
env InstanceContext
ctx [SourceType]
kinds [SourceType
a, SourceType
b] = do
let coercibleDictsInScope :: [TypeClassDict]
coercibleDictsInScope = InstanceContext
-> Qualified (ProperName 'ClassName)
-> QualifiedBy
-> [TypeClassDict]
findDicts InstanceContext
ctx Qualified (ProperName 'ClassName)
C.Coercible QualifiedBy
ByNullSourcePos
givens :: [(SourceType, SourceType)]
givens = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe [TypeClassDict]
coercibleDictsInScope forall a b. (a -> b) -> a -> b
$ \case
TypeClassDict
dict | [SourceType
a', SourceType
b'] <- forall v. TypeClassDictionaryInScope v -> [SourceType]
tcdInstanceTypes TypeClassDict
dict -> forall a. a -> Maybe a
Just (SourceType
a', SourceType
b')
| Bool
otherwise -> forall a. Maybe a
Nothing
GivenSolverState{ [(SourceType, SourceType, SourceType)]
$sel:inertGivens:GivenSolverState :: GivenSolverState -> [(SourceType, SourceType, SourceType)]
inertGivens :: [(SourceType, SourceType, SourceType)]
inertGivens } <- forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (forall (m :: * -> *).
(MonadError MultipleErrors m, MonadState CheckState m) =>
Environment -> StateT GivenSolverState m ()
solveGivens Environment
env) forall a b. (a -> b) -> a -> b
$
[(SourceType, SourceType)] -> GivenSolverState
initialGivenSolverState [(SourceType, SourceType)]
givens
(WantedSolverState{ [(SourceType, SourceType, SourceType)]
$sel:inertWanteds:WantedSolverState :: WantedSolverState -> [(SourceType, SourceType, SourceType)]
inertWanteds :: [(SourceType, SourceType, SourceType)]
inertWanteds }, [ErrorMessageHint]
hints') <- forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (forall (m :: * -> *).
(MonadError MultipleErrors m, MonadWriter [ErrorMessageHint] m,
MonadState CheckState m) =>
Environment -> StateT WantedSolverState m ()
solveWanteds Environment
env) forall a b. (a -> b) -> a -> b
$
[(SourceType, SourceType, SourceType)]
-> SourceType -> SourceType -> WantedSolverState
initialWantedSolverState [(SourceType, SourceType, SourceType)]
inertGivens SourceType
a SourceType
b
forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id ErrorMessageHint -> MultipleErrors -> MultipleErrors
addHint (forall a. [a] -> Maybe a
listToMaybe [ErrorMessageHint]
hints') forall e (m :: * -> *) a. MonadError e m => (e -> e) -> m a -> m a
`rethrow` case [(SourceType, SourceType, SourceType)]
inertWanteds of
[] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.Coercible [] [SourceType]
kinds [SourceType
a, SourceType
b] forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
(SourceType
k, SourceType
a', SourceType
b') : [(SourceType, SourceType, SourceType)]
_ | SourceType
a' forall a. Eq a => a -> a -> Bool
== SourceType
b Bool -> Bool -> Bool
&& SourceType
b' forall a. Eq a => a -> a -> Bool
== SourceType
a -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType -> SourceType -> MultipleErrors
insoluble SourceType
k SourceType
b' SourceType
a'
(SourceType
k, SourceType
a', SourceType
b') : [(SourceType, SourceType, SourceType)]
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType -> SourceType -> MultipleErrors
insoluble SourceType
k SourceType
a' SourceType
b'
solveCoercible Environment
_ InstanceContext
_ [SourceType]
_ [SourceType]
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
solveIsSymbol :: [SourceType] -> Maybe [TypeClassDict]
solveIsSymbol :: [SourceType] -> Maybe [TypeClassDict]
solveIsSymbol [TypeLevelString (SourceSpan, [Comment])
ann PSString
sym] = forall a. a -> Maybe a
Just [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 (PSString -> Evidence
IsSymbolInstance PSString
sym) [] Qualified (ProperName 'ClassName)
C.IsSymbol [] [] [forall a. a -> PSString -> Type a
TypeLevelString (SourceSpan, [Comment])
ann PSString
sym] forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
solveIsSymbol [SourceType]
_ = forall a. Maybe a
Nothing
solveSymbolCompare :: [SourceType] -> Maybe [TypeClassDict]
solveSymbolCompare :: [SourceType] -> Maybe [TypeClassDict]
solveSymbolCompare [arg0 :: SourceType
arg0@(TypeLevelString (SourceSpan, [Comment])
_ PSString
lhs), arg1 :: SourceType
arg1@(TypeLevelString (SourceSpan, [Comment])
_ PSString
rhs), SourceType
_] =
let ordering :: Qualified (ProperName 'TypeName)
ordering = case forall a. Ord a => a -> a -> Ordering
compare PSString
lhs PSString
rhs of
Ordering
LT -> Qualified (ProperName 'TypeName)
C.LT
Ordering
EQ -> Qualified (ProperName 'TypeName)
C.EQ
Ordering
GT -> Qualified (ProperName 'TypeName)
C.GT
args' :: [SourceType]
args' = [SourceType
arg0, SourceType
arg1, Qualified (ProperName 'TypeName) -> SourceType
srcTypeConstructor Qualified (ProperName 'TypeName)
ordering]
in forall a. a -> Maybe a
Just [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.SymbolCompare [] [] [SourceType]
args' forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
solveSymbolCompare [SourceType]
_ = forall a. Maybe a
Nothing
solveSymbolAppend :: [SourceType] -> Maybe [TypeClassDict]
solveSymbolAppend :: [SourceType] -> Maybe [TypeClassDict]
solveSymbolAppend [SourceType
arg0, SourceType
arg1, SourceType
arg2] = do
(SourceType
arg0', SourceType
arg1', SourceType
arg2') <- SourceType
-> SourceType
-> SourceType
-> Maybe (SourceType, SourceType, SourceType)
appendSymbols SourceType
arg0 SourceType
arg1 SourceType
arg2
let args' :: [SourceType]
args' = [SourceType
arg0', SourceType
arg1', SourceType
arg2']
forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.SymbolAppend [] [] [SourceType]
args' forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
solveSymbolAppend [SourceType]
_ = forall a. Maybe a
Nothing
appendSymbols :: SourceType -> SourceType -> SourceType -> Maybe (SourceType, SourceType, SourceType)
appendSymbols :: SourceType
-> SourceType
-> SourceType
-> Maybe (SourceType, SourceType, SourceType)
appendSymbols arg0 :: SourceType
arg0@(TypeLevelString (SourceSpan, [Comment])
_ PSString
lhs) arg1 :: SourceType
arg1@(TypeLevelString (SourceSpan, [Comment])
_ PSString
rhs) SourceType
_ = forall a. a -> Maybe a
Just (SourceType
arg0, SourceType
arg1, PSString -> SourceType
srcTypeLevelString (PSString
lhs forall a. Semigroup a => a -> a -> a
<> PSString
rhs))
appendSymbols arg0 :: SourceType
arg0@(TypeLevelString (SourceSpan, [Comment])
_ PSString
lhs) SourceType
_ arg2 :: SourceType
arg2@(TypeLevelString (SourceSpan, [Comment])
_ PSString
out) = do
Text
lhs' <- PSString -> Maybe Text
decodeString PSString
lhs
Text
out' <- PSString -> Maybe Text
decodeString PSString
out
Text
rhs <- Text -> Text -> Maybe Text
stripPrefix Text
lhs' Text
out'
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
arg0, PSString -> SourceType
srcTypeLevelString (Text -> PSString
mkString Text
rhs), SourceType
arg2)
appendSymbols SourceType
_ arg1 :: SourceType
arg1@(TypeLevelString (SourceSpan, [Comment])
_ PSString
rhs) arg2 :: SourceType
arg2@(TypeLevelString (SourceSpan, [Comment])
_ PSString
out) = do
Text
rhs' <- PSString -> Maybe Text
decodeString PSString
rhs
Text
out' <- PSString -> Maybe Text
decodeString PSString
out
Text
lhs <- Text -> Text -> Maybe Text
stripSuffix Text
rhs' Text
out'
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PSString -> SourceType
srcTypeLevelString (Text -> PSString
mkString Text
lhs), SourceType
arg1, SourceType
arg2)
appendSymbols SourceType
_ SourceType
_ SourceType
_ = forall a. Maybe a
Nothing
solveSymbolCons :: [SourceType] -> Maybe [TypeClassDict]
solveSymbolCons :: [SourceType] -> Maybe [TypeClassDict]
solveSymbolCons [SourceType
arg0, SourceType
arg1, SourceType
arg2] = do
(SourceType
arg0', SourceType
arg1', SourceType
arg2') <- SourceType
-> SourceType
-> SourceType
-> Maybe (SourceType, SourceType, SourceType)
consSymbol SourceType
arg0 SourceType
arg1 SourceType
arg2
let args' :: [SourceType]
args' = [SourceType
arg0', SourceType
arg1', SourceType
arg2']
forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.SymbolCons [] [] [SourceType]
args' forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
solveSymbolCons [SourceType]
_ = forall a. Maybe a
Nothing
consSymbol :: SourceType -> SourceType -> SourceType -> Maybe (SourceType, SourceType, SourceType)
consSymbol :: SourceType
-> SourceType
-> SourceType
-> Maybe (SourceType, SourceType, SourceType)
consSymbol SourceType
_ SourceType
_ arg :: SourceType
arg@(TypeLevelString (SourceSpan, [Comment])
_ PSString
s) = do
(Char
h, Text
t) <- Text -> Maybe (Char, Text)
T.uncons forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< PSString -> Maybe Text
decodeString PSString
s
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> SourceType
mkTLString (Char -> Text
T.singleton Char
h), Text -> SourceType
mkTLString Text
t, SourceType
arg)
where mkTLString :: Text -> SourceType
mkTLString = PSString -> SourceType
srcTypeLevelString forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> PSString
mkString
consSymbol arg1 :: SourceType
arg1@(TypeLevelString (SourceSpan, [Comment])
_ PSString
h) arg2 :: SourceType
arg2@(TypeLevelString (SourceSpan, [Comment])
_ PSString
t) SourceType
_ = do
Text
h' <- PSString -> Maybe Text
decodeString PSString
h
Text
t' <- PSString -> Maybe Text
decodeString PSString
t
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Text -> Int
T.length Text
h' forall a. Eq a => a -> a -> Bool
== Int
1)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
arg1, SourceType
arg2, PSString -> SourceType
srcTypeLevelString (Text -> PSString
mkString forall a b. (a -> b) -> a -> b
$ Text
h' forall a. Semigroup a => a -> a -> a
<> Text
t'))
consSymbol SourceType
_ SourceType
_ SourceType
_ = forall a. Maybe a
Nothing
solveIntToString :: [SourceType] -> Maybe [TypeClassDict]
solveIntToString :: [SourceType] -> Maybe [TypeClassDict]
solveIntToString [SourceType
arg0, SourceType
_] = do
(SourceType
arg0', SourceType
arg1') <- SourceType -> Maybe (SourceType, SourceType)
printIntToString SourceType
arg0
let args' :: [SourceType]
args' = [SourceType
arg0', SourceType
arg1']
forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.IntToString [] [] [SourceType]
args' forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
solveIntToString [SourceType]
_ = forall a. Maybe a
Nothing
printIntToString :: SourceType -> Maybe (SourceType, SourceType)
printIntToString :: SourceType -> Maybe (SourceType, SourceType)
printIntToString arg0 :: SourceType
arg0@(TypeLevelInt (SourceSpan, [Comment])
_ Integer
i) = do
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
arg0, PSString -> SourceType
srcTypeLevelString forall a b. (a -> b) -> a -> b
$ Text -> PSString
mkString forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Integer
i)
printIntToString SourceType
_ = forall a. Maybe a
Nothing
solveReflectable :: [SourceType] -> Maybe [TypeClassDict]
solveReflectable :: [SourceType] -> Maybe [TypeClassDict]
solveReflectable [SourceType
typeLevel, SourceType
_] = do
(Reflectable
ref, SourceType
typ) <- case SourceType
typeLevel of
TypeLevelInt (SourceSpan, [Comment])
_ Integer
i -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Reflectable
ReflectableInt Integer
i, SourceType
tyInt)
TypeLevelString (SourceSpan, [Comment])
_ PSString
s -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (PSString -> Reflectable
ReflectableString PSString
s, SourceType
tyString)
TypeConstructor (SourceSpan, [Comment])
_ Qualified (ProperName 'TypeName)
n
| Qualified (ProperName 'TypeName)
n forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'TypeName)
C.True -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Reflectable
ReflectableBoolean Bool
True, SourceType
tyBoolean)
| Qualified (ProperName 'TypeName)
n forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'TypeName)
C.False -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Reflectable
ReflectableBoolean Bool
False, SourceType
tyBoolean)
| Qualified (ProperName 'TypeName)
n forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'TypeName)
C.LT -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ordering -> Reflectable
ReflectableOrdering Ordering
LT, Qualified (ProperName 'TypeName) -> SourceType
srcTypeConstructor Qualified (ProperName 'TypeName)
C.Ordering)
| Qualified (ProperName 'TypeName)
n forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'TypeName)
C.EQ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ordering -> Reflectable
ReflectableOrdering Ordering
EQ, Qualified (ProperName 'TypeName) -> SourceType
srcTypeConstructor Qualified (ProperName 'TypeName)
C.Ordering)
| Qualified (ProperName 'TypeName)
n forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'TypeName)
C.GT -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ordering -> Reflectable
ReflectableOrdering Ordering
GT, Qualified (ProperName 'TypeName) -> SourceType
srcTypeConstructor Qualified (ProperName 'TypeName)
C.Ordering)
SourceType
_ -> forall a. Maybe a
Nothing
forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 (Reflectable -> Evidence
ReflectableInstance Reflectable
ref) [] Qualified (ProperName 'ClassName)
C.Reflectable [] [] [SourceType
typeLevel, SourceType
typ] forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
solveReflectable [SourceType]
_ = forall a. Maybe a
Nothing
solveIntAdd :: [SourceType] -> Maybe [TypeClassDict]
solveIntAdd :: [SourceType] -> Maybe [TypeClassDict]
solveIntAdd [SourceType
arg0, SourceType
arg1, SourceType
arg2] = do
(SourceType
arg0', SourceType
arg1', SourceType
arg2') <- SourceType
-> SourceType
-> SourceType
-> Maybe (SourceType, SourceType, SourceType)
addInts SourceType
arg0 SourceType
arg1 SourceType
arg2
let args' :: [SourceType]
args' = [SourceType
arg0', SourceType
arg1', SourceType
arg2']
forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.IntAdd [] [] [SourceType]
args' forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
solveIntAdd [SourceType]
_ = forall a. Maybe a
Nothing
addInts :: SourceType -> SourceType -> SourceType -> Maybe (SourceType, SourceType, SourceType)
addInts :: SourceType
-> SourceType
-> SourceType
-> Maybe (SourceType, SourceType, SourceType)
addInts arg0 :: SourceType
arg0@(TypeLevelInt (SourceSpan, [Comment])
_ Integer
l) arg1 :: SourceType
arg1@(TypeLevelInt (SourceSpan, [Comment])
_ Integer
r) SourceType
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
arg0, SourceType
arg1, Integer -> SourceType
srcTypeLevelInt (Integer
l forall a. Num a => a -> a -> a
+ Integer
r))
addInts arg0 :: SourceType
arg0@(TypeLevelInt (SourceSpan, [Comment])
_ Integer
l) SourceType
_ arg2 :: SourceType
arg2@(TypeLevelInt (SourceSpan, [Comment])
_ Integer
o) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
arg0, Integer -> SourceType
srcTypeLevelInt (Integer
o forall a. Num a => a -> a -> a
- Integer
l), SourceType
arg2)
addInts SourceType
_ arg1 :: SourceType
arg1@(TypeLevelInt (SourceSpan, [Comment])
_ Integer
r) arg2 :: SourceType
arg2@(TypeLevelInt (SourceSpan, [Comment])
_ Integer
o) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SourceType
srcTypeLevelInt (Integer
o forall a. Num a => a -> a -> a
- Integer
r), SourceType
arg1, SourceType
arg2)
addInts SourceType
_ SourceType
_ SourceType
_ = forall a. Maybe a
Nothing
solveIntCompare :: InstanceContext -> [SourceType] -> Maybe [TypeClassDict]
solveIntCompare :: InstanceContext -> [SourceType] -> Maybe [TypeClassDict]
solveIntCompare InstanceContext
_ [arg0 :: SourceType
arg0@(TypeLevelInt (SourceSpan, [Comment])
_ Integer
a), arg1 :: SourceType
arg1@(TypeLevelInt (SourceSpan, [Comment])
_ Integer
b), SourceType
_] =
let ordering :: Qualified (ProperName 'TypeName)
ordering = case forall a. Ord a => a -> a -> Ordering
compare Integer
a Integer
b of
Ordering
EQ -> Qualified (ProperName 'TypeName)
C.EQ
Ordering
LT -> Qualified (ProperName 'TypeName)
C.LT
Ordering
GT -> Qualified (ProperName 'TypeName)
C.GT
args' :: [SourceType]
args' = [SourceType
arg0, SourceType
arg1, Qualified (ProperName 'TypeName) -> SourceType
srcTypeConstructor Qualified (ProperName 'TypeName)
ordering]
in forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.IntCompare [] [] [SourceType]
args' forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
solveIntCompare InstanceContext
ctx args :: [SourceType]
args@[SourceType
a, SourceType
b, SourceType
_] = do
let compareDictsInScope :: [TypeClassDict]
compareDictsInScope = InstanceContext
-> Qualified (ProperName 'ClassName)
-> QualifiedBy
-> [TypeClassDict]
findDicts InstanceContext
ctx Qualified (ProperName 'ClassName)
C.IntCompare QualifiedBy
ByNullSourcePos
givens :: Context SourceType
givens = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe [TypeClassDict]
compareDictsInScope forall a b. (a -> b) -> a -> b
$ \case
TypeClassDict
dict | [SourceType
a', SourceType
b', SourceType
c'] <- forall v. TypeClassDictionaryInScope v -> [SourceType]
tcdInstanceTypes TypeClassDict
dict -> forall a. Type a -> Type a -> Type a -> Maybe (Relation (Type a))
mkRelation SourceType
a' SourceType
b' SourceType
c'
| Bool
otherwise -> forall a. Maybe a
Nothing
facts :: Context SourceType
facts = forall a. [[Type a]] -> [Relation (Type a)]
mkFacts ([SourceType]
args forall a. a -> [a] -> [a]
: (forall v. TypeClassDictionaryInScope v -> [SourceType]
tcdInstanceTypes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TypeClassDict]
compareDictsInScope))
Qualified (ProperName 'TypeName)
c' <- forall a.
Ord a =>
Context a -> a -> a -> Maybe (Qualified (ProperName 'TypeName))
solveRelation (Context SourceType
givens forall a. Semigroup a => a -> a -> a
<> Context SourceType
facts) SourceType
a SourceType
b
forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.IntCompare [] [] [SourceType
a, SourceType
b, Qualified (ProperName 'TypeName) -> SourceType
srcTypeConstructor Qualified (ProperName 'TypeName)
c'] forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
solveIntCompare InstanceContext
_ [SourceType]
_ = forall a. Maybe a
Nothing
solveIntMul :: [SourceType] -> Maybe [TypeClassDict]
solveIntMul :: [SourceType] -> Maybe [TypeClassDict]
solveIntMul [arg0 :: SourceType
arg0@(TypeLevelInt (SourceSpan, [Comment])
_ Integer
l), arg1 :: SourceType
arg1@(TypeLevelInt (SourceSpan, [Comment])
_ Integer
r), SourceType
_] =
let args' :: [SourceType]
args' = [SourceType
arg0, SourceType
arg1, Integer -> SourceType
srcTypeLevelInt (Integer
l forall a. Num a => a -> a -> a
* Integer
r)]
in forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.IntMul [] [] [SourceType]
args' forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
solveIntMul [SourceType]
_ = forall a. Maybe a
Nothing
solveUnion :: [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
solveUnion :: [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
solveUnion [SourceType]
kinds [SourceType
l, SourceType
r, SourceType
u] = do
(SourceType
lOut, SourceType
rOut, SourceType
uOut, Maybe [SourceConstraint]
cst, [(Text, SourceType)]
vars) <- [SourceType]
-> SourceType
-> SourceType
-> SourceType
-> Maybe
(SourceType, SourceType, SourceType, Maybe [SourceConstraint],
[(Text, SourceType)])
unionRows [SourceType]
kinds SourceType
l SourceType
r SourceType
u
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.RowUnion [(Text, SourceType)]
vars [SourceType]
kinds [SourceType
lOut, SourceType
rOut, SourceType
uOut] Maybe [SourceConstraint]
cst forall a. Maybe a
Nothing ]
solveUnion [SourceType]
_ [SourceType]
_ = forall a. Maybe a
Nothing
unionRows :: [SourceType] -> SourceType -> SourceType -> SourceType -> Maybe (SourceType, SourceType, SourceType, Maybe [SourceConstraint], [(Text, SourceType)])
unionRows :: [SourceType]
-> SourceType
-> SourceType
-> SourceType
-> Maybe
(SourceType, SourceType, SourceType, Maybe [SourceConstraint],
[(Text, SourceType)])
unionRows [SourceType]
kinds SourceType
l SourceType
r SourceType
u =
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
canMakeProgress forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> (SourceType
lOut, SourceType
rOut, SourceType
uOut, Maybe [SourceConstraint]
cons, [(Text, SourceType)]
vars)
where
([RowListItem (SourceSpan, [Comment])]
fixed, SourceType
rest) = forall a. Type a -> ([RowListItem a], Type a)
rowToList SourceType
l
rowVar :: SourceType
rowVar = Text -> SourceType
srcTypeVar Text
"r"
(Bool
canMakeProgress, SourceType
lOut, SourceType
rOut, SourceType
uOut, Maybe [SourceConstraint]
cons, [(Text, SourceType)]
vars) =
case SourceType
rest of
REmptyKinded (SourceSpan, [Comment])
_ Maybe SourceType
_ -> (Bool
True, SourceType
l, SourceType
r, forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem (SourceSpan, [Comment])]
fixed, SourceType
r), forall a. Maybe a
Nothing, [])
SourceType
_ | ([RowListItem (SourceSpan, [Comment])]
right, rightu :: SourceType
rightu@(REmptyKinded (SourceSpan, [Comment])
_ Maybe SourceType
_)) <- forall a. Type a -> ([RowListItem a], Type a)
rowToList SourceType
r
, ([RowListItem (SourceSpan, [Comment])]
output, restu :: SourceType
restu@(REmptyKinded (SourceSpan, [Comment])
_ Maybe SourceType
_)) <- forall a. Type a -> ([RowListItem a], Type a)
rowToList SourceType
u ->
let
grabLabel :: RowListItem a
-> ([RowListItem a], [RowListItem a], [Label])
-> ([RowListItem a], [RowListItem a], [Label])
grabLabel RowListItem a
e ([RowListItem a]
left', [RowListItem a]
right', [Label]
remaining)
| forall a. RowListItem a -> Label
rowListLabel RowListItem a
e forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Label]
remaining =
([RowListItem a]
left', RowListItem a
e forall a. a -> [a] -> [a]
: [RowListItem a]
right', forall a. Eq a => a -> [a] -> [a]
delete (forall a. RowListItem a -> Label
rowListLabel RowListItem a
e) [Label]
remaining)
| Bool
otherwise =
(RowListItem a
e forall a. a -> [a] -> [a]
: [RowListItem a]
left', [RowListItem a]
right', [Label]
remaining)
([RowListItem (SourceSpan, [Comment])]
outL, [RowListItem (SourceSpan, [Comment])]
outR, [Label]
leftover) =
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall {a}.
RowListItem a
-> ([RowListItem a], [RowListItem a], [Label])
-> ([RowListItem a], [RowListItem a], [Label])
grabLabel ([], [], forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. RowListItem a -> Label
rowListLabel [RowListItem (SourceSpan, [Comment])]
right) [RowListItem (SourceSpan, [Comment])]
output
in ( forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Label]
leftover
, forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem (SourceSpan, [Comment])]
outL, SourceType
restu)
, forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem (SourceSpan, [Comment])]
outR, SourceType
rightu)
, SourceType
u
, forall a. Maybe a
Nothing
, []
)
SourceType
_ -> ( Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RowListItem (SourceSpan, [Comment])]
fixed)
, SourceType
l, SourceType
r
, forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem (SourceSpan, [Comment])]
fixed, SourceType
rowVar)
, forall a. a -> Maybe a
Just [ Qualified (ProperName 'ClassName)
-> [SourceType]
-> [SourceType]
-> Maybe ConstraintData
-> SourceConstraint
srcConstraint Qualified (ProperName 'ClassName)
C.RowUnion [SourceType]
kinds [SourceType
rest, SourceType
r, SourceType
rowVar] forall a. Maybe a
Nothing ]
, [(Text
"r", SourceType -> SourceType
kindRow (forall a. [a] -> a
head [SourceType]
kinds))]
)
solveRowCons :: [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
solveRowCons :: [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
solveRowCons [SourceType]
kinds [TypeLevelString (SourceSpan, [Comment])
ann PSString
sym, SourceType
ty, SourceType
r, SourceType
_] =
forall a. a -> Maybe a
Just [ forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.RowCons [] [SourceType]
kinds [forall a. a -> PSString -> Type a
TypeLevelString (SourceSpan, [Comment])
ann PSString
sym, SourceType
ty, SourceType
r, Label -> SourceType -> SourceType -> SourceType
srcRCons (PSString -> Label
Label PSString
sym) SourceType
ty SourceType
r] forall a. Maybe a
Nothing forall a. Maybe a
Nothing ]
solveRowCons [SourceType]
_ [SourceType]
_ = forall a. Maybe a
Nothing
solveRowToList :: [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
solveRowToList :: [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
solveRowToList [SourceType
kind] [SourceType
r, SourceType
_] = do
SourceType
entries <- SourceType -> SourceType -> Maybe SourceType
rowToRowList SourceType
kind SourceType
r
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.RowToList [] [SourceType
kind] [SourceType
r, SourceType
entries] forall a. Maybe a
Nothing forall a. Maybe a
Nothing ]
solveRowToList [SourceType]
_ [SourceType]
_ = forall a. Maybe a
Nothing
rowToRowList :: SourceType -> SourceType -> Maybe SourceType
rowToRowList :: SourceType -> SourceType -> Maybe SourceType
rowToRowList SourceType
kind SourceType
r =
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (forall a. Type a -> Bool
isREmpty SourceType
rest) forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr RowListItem (SourceSpan, [Comment]) -> SourceType -> SourceType
rowListCons (SourceType -> SourceType -> SourceType
srcKindApp (Qualified (ProperName 'TypeName) -> SourceType
srcTypeConstructor Qualified (ProperName 'TypeName)
C.RowListNil) SourceType
kind) [RowListItem (SourceSpan, [Comment])]
fixed
where
([RowListItem (SourceSpan, [Comment])]
fixed, SourceType
rest) = forall a. Type a -> ([RowListItem a], Type a)
rowToSortedList SourceType
r
rowListCons :: RowListItem (SourceSpan, [Comment]) -> SourceType -> SourceType
rowListCons (RowListItem (SourceSpan, [Comment])
_ Label
lbl SourceType
ty) SourceType
tl =
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl SourceType -> SourceType -> SourceType
srcTypeApp (SourceType -> SourceType -> SourceType
srcKindApp (Qualified (ProperName 'TypeName) -> SourceType
srcTypeConstructor Qualified (ProperName 'TypeName)
C.RowListCons) SourceType
kind)
[ PSString -> SourceType
srcTypeLevelString (Label -> PSString
runLabel Label
lbl)
, SourceType
ty
, SourceType
tl ]
solveNub :: [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
solveNub :: [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
solveNub [SourceType]
kinds [SourceType
r, SourceType
_] = do
SourceType
r' <- SourceType -> Maybe SourceType
nubRows SourceType
r
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.RowNub [] [SourceType]
kinds [SourceType
r, SourceType
r'] forall a. Maybe a
Nothing forall a. Maybe a
Nothing ]
solveNub [SourceType]
_ [SourceType]
_ = forall a. Maybe a
Nothing
nubRows :: SourceType -> Maybe SourceType
nubRows :: SourceType -> Maybe SourceType
nubRows SourceType
r =
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (forall a. Type a -> Bool
isREmpty SourceType
rest) forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>
forall a. ([RowListItem a], Type a) -> Type a
rowFromList (forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a. RowListItem a -> Label
rowListLabel) [RowListItem (SourceSpan, [Comment])]
fixed, SourceType
rest)
where
([RowListItem (SourceSpan, [Comment])]
fixed, SourceType
rest) = forall a. Type a -> ([RowListItem a], Type a)
rowToSortedList SourceType
r
solveLacks :: [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
solveLacks :: [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
solveLacks [SourceType]
kinds tys :: [SourceType]
tys@[SourceType
_, REmptyKinded (SourceSpan, [Comment])
_ Maybe SourceType
_] =
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.RowLacks [] [SourceType]
kinds [SourceType]
tys forall a. Maybe a
Nothing forall a. Maybe a
Nothing ]
solveLacks [SourceType]
kinds [TypeLevelString (SourceSpan, [Comment])
ann PSString
sym, SourceType
r] = do
(SourceType
r', Maybe [SourceConstraint]
cst) <- [SourceType]
-> PSString
-> SourceType
-> Maybe (SourceType, Maybe [SourceConstraint])
rowLacks [SourceType]
kinds PSString
sym SourceType
r
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.RowLacks [] [SourceType]
kinds [forall a. a -> PSString -> Type a
TypeLevelString (SourceSpan, [Comment])
ann PSString
sym, SourceType
r'] Maybe [SourceConstraint]
cst forall a. Maybe a
Nothing ]
solveLacks [SourceType]
_ [SourceType]
_ = forall a. Maybe a
Nothing
rowLacks :: [SourceType] -> PSString -> SourceType -> Maybe (SourceType, Maybe [SourceConstraint])
rowLacks :: [SourceType]
-> PSString
-> SourceType
-> Maybe (SourceType, Maybe [SourceConstraint])
rowLacks [SourceType]
kinds PSString
sym SourceType
r =
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool
lacksSym Bool -> Bool -> Bool
&& Bool
canMakeProgress) forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> (SourceType
r, Maybe [SourceConstraint]
cst)
where
([RowListItem (SourceSpan, [Comment])]
fixed, SourceType
rest) = forall a. Type a -> ([RowListItem a], Type a)
rowToList SourceType
r
lacksSym :: Bool
lacksSym =
PSString
sym forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` (Label -> PSString
runLabel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. RowListItem a -> Label
rowListLabel forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RowListItem (SourceSpan, [Comment])]
fixed)
(Bool
canMakeProgress, Maybe [SourceConstraint]
cst) = case SourceType
rest of
REmptyKinded (SourceSpan, [Comment])
_ Maybe SourceType
_ -> (Bool
True, forall a. Maybe a
Nothing)
SourceType
_ -> (Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RowListItem (SourceSpan, [Comment])]
fixed), forall a. a -> Maybe a
Just [ Qualified (ProperName 'ClassName)
-> [SourceType]
-> [SourceType]
-> Maybe ConstraintData
-> SourceConstraint
srcConstraint Qualified (ProperName 'ClassName)
C.RowLacks [SourceType]
kinds [PSString -> SourceType
srcTypeLevelString PSString
sym, SourceType
rest] forall a. Maybe a
Nothing ])
matches :: [FunctionalDependency] -> TypeClassDict -> [SourceType] -> Matched (Matching [SourceType])
matches :: [FunctionalDependency]
-> TypeClassDict -> [SourceType] -> Matched (Matching [SourceType])
matches [FunctionalDependency]
deps TypeClassDictionaryInScope{Integer
[(Text, SourceType)]
[(Qualified (ProperName 'ClassName), Integer)]
[SourceType]
Maybe [SourceConstraint]
Maybe ChainId
Maybe SourceType
Qualified (ProperName 'ClassName)
Evidence
tcdDescription :: Maybe SourceType
tcdDependencies :: Maybe [SourceConstraint]
tcdInstanceTypes :: [SourceType]
tcdInstanceKinds :: [SourceType]
tcdForAll :: [(Text, SourceType)]
tcdClassName :: Qualified (ProperName 'ClassName)
tcdPath :: [(Qualified (ProperName 'ClassName), Integer)]
tcdValue :: Evidence
tcdIndex :: Integer
tcdChain :: Maybe ChainId
tcdDescription :: forall v. TypeClassDictionaryInScope v -> Maybe SourceType
tcdInstanceKinds :: forall v. TypeClassDictionaryInScope v -> [SourceType]
tcdForAll :: forall v. TypeClassDictionaryInScope v -> [(Text, SourceType)]
tcdClassName :: forall v.
TypeClassDictionaryInScope v -> Qualified (ProperName 'ClassName)
tcdPath :: forall v.
TypeClassDictionaryInScope v
-> [(Qualified (ProperName 'ClassName), Integer)]
tcdValue :: forall v. TypeClassDictionaryInScope v -> v
tcdDependencies :: forall v. TypeClassDictionaryInScope v -> Maybe [SourceConstraint]
tcdInstanceTypes :: forall v. TypeClassDictionaryInScope v -> [SourceType]
tcdIndex :: forall v. TypeClassDictionaryInScope v -> Integer
tcdChain :: forall v. TypeClassDictionaryInScope v -> Maybe ChainId
..} [SourceType]
tys =
let matched :: [(Matched (), Matching [SourceType])]
matched = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a. Type a -> Type a -> (Matched (), Matching [Type a])
typeHeadsAreEqual [SourceType]
tys [SourceType]
tcdInstanceTypes in
if Bool -> Bool
not (forall subst. [(Matched (), subst)] -> Bool
covers [(Matched (), Matching [SourceType])]
matched)
then if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Eq a => a -> a -> Bool
(==) forall t. Matched t
Apart forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Matched (), Matching [SourceType])]
matched then forall t. Matched t
Apart else forall t. Matched t
Unknown
else
let determinedSet :: Set Int
determinedSet = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall a. Ord a => [a] -> Set a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. FunctionalDependency -> [Int]
fdDetermined) [FunctionalDependency]
deps
solved :: [Matching [SourceType]]
solved = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set Int
determinedSet) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(Matched ()
_, Matching [SourceType]
ts) Int
i -> (Int
i, Matching [SourceType]
ts)) [(Matched (), Matching [SourceType])]
matched [Int
0..]
in forall a. Matching [Type a] -> Matched (Matching [Type a])
verifySubstitution (forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
M.unionsWith forall a. [a] -> [a] -> [a]
(++) [Matching [SourceType]]
solved)
where
covers :: [(Matched (), subst)] -> Bool
covers :: forall subst. [(Matched (), subst)] -> Bool
covers [(Matched (), subst)]
ms = Set Int
finalSet forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> Set a
S.fromList [Int
0..forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Matched (), subst)]
ms forall a. Num a => a -> a -> a
- Int
1]
where
initialSet :: S.Set Int
initialSet :: Set Int
initialSet = forall a. Ord a => [a] -> Set a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
(==) (forall t. t -> Matched t
Match ()) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [(Matched (), subst)]
ms [Int
0..]
finalSet :: S.Set Int
finalSet :: Set Int
finalSet = forall a. Eq a => (a -> a) -> a -> a
untilFixedPoint Set Int -> Set Int
applyAll Set Int
initialSet
untilFixedPoint :: Eq a => (a -> a) -> a -> a
untilFixedPoint :: forall a. Eq a => (a -> a) -> a -> a
untilFixedPoint a -> a
f = a -> a
go
where
go :: a -> a
go a
a | a
a' forall a. Eq a => a -> a -> Bool
== a
a = a
a'
| Bool
otherwise = a -> a
go a
a'
where a' :: a
a' = a -> a
f a
a
applyAll :: S.Set Int -> S.Set Int
applyAll :: Set Int -> Set Int
applyAll Set Int
s = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr FunctionalDependency -> Set Int -> Set Int
applyDependency Set Int
s [FunctionalDependency]
deps
applyDependency :: FunctionalDependency -> S.Set Int -> S.Set Int
applyDependency :: FunctionalDependency -> Set Int -> Set Int
applyDependency FunctionalDependency{[Int]
fdDeterminers :: FunctionalDependency -> [Int]
fdDetermined :: [Int]
fdDeterminers :: [Int]
fdDetermined :: FunctionalDependency -> [Int]
..} Set Int
xs
| forall a. Ord a => [a] -> Set a
S.fromList [Int]
fdDeterminers forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` Set Int
xs = Set Int
xs forall a. Semigroup a => a -> a -> a
<> forall a. Ord a => [a] -> Set a
S.fromList [Int]
fdDetermined
| Bool
otherwise = Set Int
xs
typeHeadsAreEqual :: Type a -> Type a -> (Matched (), Matching [Type a])
typeHeadsAreEqual :: forall a. Type a -> Type a -> (Matched (), Matching [Type a])
typeHeadsAreEqual (KindedType a
_ Type a
t1 Type a
_) Type a
t2 = forall a. Type a -> Type a -> (Matched (), Matching [Type a])
typeHeadsAreEqual Type a
t1 Type a
t2
typeHeadsAreEqual Type a
t1 (KindedType a
_ Type a
t2 Type a
_) = forall a. Type a -> Type a -> (Matched (), Matching [Type a])
typeHeadsAreEqual Type a
t1 Type a
t2
typeHeadsAreEqual (TUnknown a
_ Int
u1) (TUnknown a
_ Int
u2) | Int
u1 forall a. Eq a => a -> a -> Bool
== Int
u2 = (forall t. t -> Matched t
Match (), forall k a. Map k a
M.empty)
typeHeadsAreEqual (Skolem a
_ Text
_ Maybe (Type a)
_ Int
s1 SkolemScope
_) (Skolem a
_ Text
_ Maybe (Type a)
_ Int
s2 SkolemScope
_) | Int
s1 forall a. Eq a => a -> a -> Bool
== Int
s2 = (forall t. t -> Matched t
Match (), forall k a. Map k a
M.empty)
typeHeadsAreEqual Type a
t (TypeVar a
_ Text
v) = (forall t. t -> Matched t
Match (), forall k a. k -> a -> Map k a
M.singleton Text
v [Type a
t])
typeHeadsAreEqual (TypeConstructor a
_ Qualified (ProperName 'TypeName)
c1) (TypeConstructor a
_ Qualified (ProperName 'TypeName)
c2) | Qualified (ProperName 'TypeName)
c1 forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'TypeName)
c2 = (forall t. t -> Matched t
Match (), forall k a. Map k a
M.empty)
typeHeadsAreEqual (TypeLevelString a
_ PSString
s1) (TypeLevelString a
_ PSString
s2) | PSString
s1 forall a. Eq a => a -> a -> Bool
== PSString
s2 = (forall t. t -> Matched t
Match (), forall k a. Map k a
M.empty)
typeHeadsAreEqual (TypeLevelInt a
_ Integer
n1) (TypeLevelInt a
_ Integer
n2) | Integer
n1 forall a. Eq a => a -> a -> Bool
== Integer
n2 = (forall t. t -> Matched t
Match (), forall k a. Map k a
M.empty)
typeHeadsAreEqual (TypeApp a
_ Type a
h1 Type a
t1) (TypeApp a
_ Type a
h2 Type a
t2) =
forall a.
(Matched (), Matching [Type a])
-> (Matched (), Matching [Type a])
-> (Matched (), Matching [Type a])
both (forall a. Type a -> Type a -> (Matched (), Matching [Type a])
typeHeadsAreEqual Type a
h1 Type a
h2) (forall a. Type a -> Type a -> (Matched (), Matching [Type a])
typeHeadsAreEqual Type a
t1 Type a
t2)
typeHeadsAreEqual (KindApp a
_ Type a
h1 Type a
t1) (KindApp a
_ Type a
h2 Type a
t2) =
forall a.
(Matched (), Matching [Type a])
-> (Matched (), Matching [Type a])
-> (Matched (), Matching [Type a])
both (forall a. Type a -> Type a -> (Matched (), Matching [Type a])
typeHeadsAreEqual Type a
h1 Type a
h2) (forall a. Type a -> Type a -> (Matched (), Matching [Type a])
typeHeadsAreEqual Type a
t1 Type a
t2)
typeHeadsAreEqual (REmpty a
_) (REmpty a
_) = (forall t. t -> Matched t
Match (), forall k a. Map k a
M.empty)
typeHeadsAreEqual r1 :: Type a
r1@RCons{} r2 :: Type a
r2@RCons{} =
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a.
(Matched (), Matching [Type a])
-> (Matched (), Matching [Type a])
-> (Matched (), Matching [Type a])
both (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a.
([RowListItem a], Type a)
-> ([RowListItem a], Type a) -> (Matched (), Matching [Type a])
go (([RowListItem a], Type a), ([RowListItem a], Type a))
rest) [(Matched (), Matching [Type a])]
common
where
([(Matched (), Matching [Type a])]
common, (([RowListItem a], Type a), ([RowListItem a], Type a))
rest) = forall a r.
(Label -> Type a -> Type a -> r)
-> Type a
-> Type a
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
alignRowsWith (forall a b. a -> b -> a
const forall a. Type a -> Type a -> (Matched (), Matching [Type a])
typeHeadsAreEqual) Type a
r1 Type a
r2
go :: ([RowListItem a], Type a) -> ([RowListItem a], Type a) -> (Matched (), Matching [Type a])
go :: forall a.
([RowListItem a], Type a)
-> ([RowListItem a], Type a) -> (Matched (), Matching [Type a])
go ([RowListItem a]
l, KindedType a
_ Type a
t1 Type a
_) ([RowListItem a]
r, Type a
t2) = forall a.
([RowListItem a], Type a)
-> ([RowListItem a], Type a) -> (Matched (), Matching [Type a])
go ([RowListItem a]
l, Type a
t1) ([RowListItem a]
r, Type a
t2)
go ([RowListItem a]
l, Type a
t1) ([RowListItem a]
r, KindedType a
_ Type a
t2 Type a
_) = forall a.
([RowListItem a], Type a)
-> ([RowListItem a], Type a) -> (Matched (), Matching [Type a])
go ([RowListItem a]
l, Type a
t1) ([RowListItem a]
r, Type a
t2)
go ([RowListItem a]
l, KindApp a
_ Type a
t1 Type a
k1) ([RowListItem a]
r, KindApp a
_ Type a
t2 Type a
k2) | forall a b. Type a -> Type b -> Bool
eqType Type a
k1 Type a
k2 = forall a.
([RowListItem a], Type a)
-> ([RowListItem a], Type a) -> (Matched (), Matching [Type a])
go ([RowListItem a]
l, Type a
t1) ([RowListItem a]
r, Type a
t2)
go ([], REmpty a
_) ([], REmpty a
_) = (forall t. t -> Matched t
Match (), forall k a. Map k a
M.empty)
go ([], TUnknown a
_ Int
u1) ([], TUnknown a
_ Int
u2) | Int
u1 forall a. Eq a => a -> a -> Bool
== Int
u2 = (forall t. t -> Matched t
Match (), forall k a. Map k a
M.empty)
go ([], TypeVar a
_ Text
v1) ([], TypeVar a
_ Text
v2) | Text
v1 forall a. Eq a => a -> a -> Bool
== Text
v2 = (forall t. t -> Matched t
Match (), forall k a. Map k a
M.empty)
go ([], Skolem a
_ Text
_ Maybe (Type a)
_ Int
sk1 SkolemScope
_) ([], Skolem a
_ Text
_ Maybe (Type a)
_ Int
sk2 SkolemScope
_) | Int
sk1 forall a. Eq a => a -> a -> Bool
== Int
sk2 = (forall t. t -> Matched t
Match (), forall k a. Map k a
M.empty)
go ([], TUnknown a
_ Int
_) ([RowListItem a], Type a)
_ = (forall t. Matched t
Unknown, forall k a. Map k a
M.empty)
go ([RowListItem a]
sd, Type a
r) ([], TypeVar a
_ Text
v) = (forall t. t -> Matched t
Match (), forall k a. k -> a -> Map k a
M.singleton Text
v [forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem a]
sd, Type a
r)])
go ([RowListItem a], Type a)
_ ([RowListItem a], Type a)
_ = (forall t. Matched t
Apart, forall k a. Map k a
M.empty)
typeHeadsAreEqual (TUnknown a
_ Int
_) Type a
_ = (forall t. Matched t
Unknown, forall k a. Map k a
M.empty)
typeHeadsAreEqual Skolem{} Type a
_ = (forall t. Matched t
Unknown, forall k a. Map k a
M.empty)
typeHeadsAreEqual Type a
_ Type a
_ = (forall t. Matched t
Apart, forall k a. Map k a
M.empty)
both :: (Matched (), Matching [Type a]) -> (Matched (), Matching [Type a]) -> (Matched (), Matching [Type a])
both :: forall a.
(Matched (), Matching [Type a])
-> (Matched (), Matching [Type a])
-> (Matched (), Matching [Type a])
both (Matched ()
b1, Matching [Type a]
m1) (Matched ()
b2, Matching [Type a]
m2) = (Matched ()
b1 forall a. Semigroup a => a -> a -> a
<> Matched ()
b2, forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith forall a. [a] -> [a] -> [a]
(++) Matching [Type a]
m1 Matching [Type a]
m2)
verifySubstitution :: Matching [Type a] -> Matched (Matching [Type a])
verifySubstitution :: forall a. Matching [Type a] -> Matched (Matching [Type a])
verifySubstitution Matching [Type a]
mts = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall {a}. [Type a] -> Matched ()
meet Matching [Type a]
mts forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Matching [Type a]
mts where
meet :: [Type a] -> Matched ()
meet = forall m a. Monoid m => (a -> a -> m) -> [a] -> m
pairwiseAll forall a. Type a -> Type a -> Matched ()
typesAreEqual
typesAreEqual :: Type a -> Type a -> Matched ()
typesAreEqual :: forall a. Type a -> Type a -> Matched ()
typesAreEqual (KindedType a
_ Type a
t1 Type a
_) Type a
t2 = forall a. Type a -> Type a -> Matched ()
typesAreEqual Type a
t1 Type a
t2
typesAreEqual Type a
t1 (KindedType a
_ Type a
t2 Type a
_) = forall a. Type a -> Type a -> Matched ()
typesAreEqual Type a
t1 Type a
t2
typesAreEqual (TUnknown a
_ Int
u1) (TUnknown a
_ Int
u2) | Int
u1 forall a. Eq a => a -> a -> Bool
== Int
u2 = forall t. t -> Matched t
Match ()
typesAreEqual (TUnknown a
_ Int
u1) Type a
t2 = if Type a
t2 forall a. Type a -> Int -> Bool
`containsUnknown` Int
u1 then forall t. Matched t
Apart else forall t. Matched t
Unknown
typesAreEqual Type a
t1 (TUnknown a
_ Int
u2) = if Type a
t1 forall a. Type a -> Int -> Bool
`containsUnknown` Int
u2 then forall t. Matched t
Apart else forall t. Matched t
Unknown
typesAreEqual (Skolem a
_ Text
_ Maybe (Type a)
_ Int
s1 SkolemScope
_) (Skolem a
_ Text
_ Maybe (Type a)
_ Int
s2 SkolemScope
_) | Int
s1 forall a. Eq a => a -> a -> Bool
== Int
s2 = forall t. t -> Matched t
Match ()
typesAreEqual (Skolem a
_ Text
_ Maybe (Type a)
_ Int
s1 SkolemScope
_) Type a
t2 = if Type a
t2 forall a. Type a -> Int -> Bool
`containsSkolem` Int
s1 then forall t. Matched t
Apart else forall t. Matched t
Unknown
typesAreEqual Type a
t1 (Skolem a
_ Text
_ Maybe (Type a)
_ Int
s2 SkolemScope
_) = if Type a
t1 forall a. Type a -> Int -> Bool
`containsSkolem` Int
s2 then forall t. Matched t
Apart else forall t. Matched t
Unknown
typesAreEqual (TypeVar a
_ Text
v1) (TypeVar a
_ Text
v2) | Text
v1 forall a. Eq a => a -> a -> Bool
== Text
v2 = forall t. t -> Matched t
Match ()
typesAreEqual (TypeLevelString a
_ PSString
s1) (TypeLevelString a
_ PSString
s2) | PSString
s1 forall a. Eq a => a -> a -> Bool
== PSString
s2 = forall t. t -> Matched t
Match ()
typesAreEqual (TypeLevelInt a
_ Integer
n1) (TypeLevelInt a
_ Integer
n2) | Integer
n1 forall a. Eq a => a -> a -> Bool
== Integer
n2 = forall t. t -> Matched t
Match ()
typesAreEqual (TypeConstructor a
_ Qualified (ProperName 'TypeName)
c1) (TypeConstructor a
_ Qualified (ProperName 'TypeName)
c2) | Qualified (ProperName 'TypeName)
c1 forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'TypeName)
c2 = forall t. t -> Matched t
Match ()
typesAreEqual (TypeApp a
_ Type a
h1 Type a
t1) (TypeApp a
_ Type a
h2 Type a
t2) = forall a. Type a -> Type a -> Matched ()
typesAreEqual Type a
h1 Type a
h2 forall a. Semigroup a => a -> a -> a
<> forall a. Type a -> Type a -> Matched ()
typesAreEqual Type a
t1 Type a
t2
typesAreEqual (KindApp a
_ Type a
h1 Type a
t1) (KindApp a
_ Type a
h2 Type a
t2) = forall a. Type a -> Type a -> Matched ()
typesAreEqual Type a
h1 Type a
h2 forall a. Semigroup a => a -> a -> a
<> forall a. Type a -> Type a -> Matched ()
typesAreEqual Type a
t1 Type a
t2
typesAreEqual (REmpty a
_) (REmpty a
_) = forall t. t -> Matched t
Match ()
typesAreEqual Type a
r1 Type a
r2 | forall a. Type a -> Bool
isRCons Type a
r1 Bool -> Bool -> Bool
|| forall a. Type a -> Bool
isRCons Type a
r2 =
let ([Matched ()]
common, (([RowListItem a], Type a), ([RowListItem a], Type a))
rest) = forall a r.
(Label -> Type a -> Type a -> r)
-> Type a
-> Type a
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
alignRowsWith (forall a b. a -> b -> a
const forall a. Type a -> Type a -> Matched ()
typesAreEqual) Type a
r1 Type a
r2
in forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold [Matched ()]
common forall a. Semigroup a => a -> a -> a
<> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a.
([RowListItem a], Type a)
-> ([RowListItem a], Type a) -> Matched ()
go (([RowListItem a], Type a), ([RowListItem a], Type a))
rest
where
go :: ([RowListItem a], Type a) -> ([RowListItem a], Type a) -> Matched ()
go :: forall a.
([RowListItem a], Type a)
-> ([RowListItem a], Type a) -> Matched ()
go ([RowListItem a]
l, KindedType a
_ Type a
t1 Type a
_) ([RowListItem a]
r, Type a
t2) = forall a.
([RowListItem a], Type a)
-> ([RowListItem a], Type a) -> Matched ()
go ([RowListItem a]
l, Type a
t1) ([RowListItem a]
r, Type a
t2)
go ([RowListItem a]
l, Type a
t1) ([RowListItem a]
r, KindedType a
_ Type a
t2 Type a
_) = forall a.
([RowListItem a], Type a)
-> ([RowListItem a], Type a) -> Matched ()
go ([RowListItem a]
l, Type a
t1) ([RowListItem a]
r, Type a
t2)
go ([], KindApp a
_ Type a
t1 Type a
k1) ([], KindApp a
_ Type a
t2 Type a
k2) = forall a. Type a -> Type a -> Matched ()
typesAreEqual Type a
t1 Type a
t2 forall a. Semigroup a => a -> a -> a
<> forall a. Type a -> Type a -> Matched ()
typesAreEqual Type a
k1 Type a
k2
go ([], TUnknown a
_ Int
u1) ([], TUnknown a
_ Int
u2) | Int
u1 forall a. Eq a => a -> a -> Bool
== Int
u2 = forall t. t -> Matched t
Match ()
go ([], TUnknown a
_ Int
_) ([], Type a
_) = forall t. Matched t
Unknown
go ([], Type a
_) ([], TUnknown a
_ Int
_) = forall t. Matched t
Unknown
go ([], Skolem a
_ Text
_ Maybe (Type a)
_ Int
s1 SkolemScope
_) ([], Skolem a
_ Text
_ Maybe (Type a)
_ Int
s2 SkolemScope
_) | Int
s1 forall a. Eq a => a -> a -> Bool
== Int
s2 = forall t. t -> Matched t
Match ()
go ([], Skolem a
_ Text
_ Maybe (Type a)
_ Int
_ SkolemScope
_) ([RowListItem a], Type a)
_ = forall t. Matched t
Unknown
go ([RowListItem a], Type a)
_ ([], Skolem a
_ Text
_ Maybe (Type a)
_ Int
_ SkolemScope
_) = forall t. Matched t
Unknown
go ([], REmpty a
_) ([], REmpty a
_) = forall t. t -> Matched t
Match ()
go ([], TypeVar a
_ Text
v1) ([], TypeVar a
_ Text
v2) | Text
v1 forall a. Eq a => a -> a -> Bool
== Text
v2 = forall t. t -> Matched t
Match ()
go ([RowListItem a], Type a)
_ ([RowListItem a], Type a)
_ = forall t. Matched t
Apart
typesAreEqual Type a
_ Type a
_ = forall t. Matched t
Apart
isRCons :: Type a -> Bool
isRCons :: forall a. Type a -> Bool
isRCons RCons{} = Bool
True
isRCons Type a
_ = Bool
False
containsSkolem :: Type a -> Int -> Bool
containsSkolem :: forall a. Type a -> Int -> Bool
containsSkolem Type a
t Int
s = forall r a. (r -> r -> r) -> (Type a -> r) -> Type a -> r
everythingOnTypes Bool -> Bool -> Bool
(||) (\case Skolem a
_ Text
_ Maybe (Type a)
_ Int
s' SkolemScope
_ -> Int
s forall a. Eq a => a -> a -> Bool
== Int
s'; Type a
_ -> Bool
False) Type a
t
containsUnknown :: Type a -> Int -> Bool
containsUnknown :: forall a. Type a -> Int -> Bool
containsUnknown Type a
t Int
u = forall r a. (r -> r -> r) -> (Type a -> r) -> Type a -> r
everythingOnTypes Bool -> Bool -> Bool
(||) (\case TUnknown a
_ Int
u' -> Int
u forall a. Eq a => a -> a -> Bool
== Int
u'; Type a
_ -> Bool
False) Type a
t
newDictionaries
:: MonadState CheckState m
=> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified Ident
-> SourceConstraint
-> m [NamedDict]
newDictionaries :: forall (m :: * -> *).
MonadState CheckState m =>
[(Qualified (ProperName 'ClassName), Integer)]
-> Qualified Ident -> SourceConstraint -> m [NamedDict]
newDictionaries [(Qualified (ProperName 'ClassName), Integer)]
path Qualified Ident
name (Constraint (SourceSpan, [Comment])
_ Qualified (ProperName 'ClassName)
className [SourceType]
instanceKinds [SourceType]
instanceTy Maybe ConstraintData
_) = do
Map (Qualified (ProperName 'ClassName)) TypeClassData
tcs <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Environment
-> Map (Qualified (ProperName 'ClassName)) TypeClassData
typeClasses forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckState -> Environment
checkEnv)
let TypeClassData{Bool
[(Text, Maybe SourceType)]
[(Ident, SourceType)]
[SourceConstraint]
[FunctionalDependency]
Set Int
Set (Set Int)
typeClassDeterminedArguments :: TypeClassData -> Set Int
typeClassSuperclasses :: TypeClassData -> [SourceConstraint]
typeClassMembers :: TypeClassData -> [(Ident, SourceType)]
typeClassArguments :: TypeClassData -> [(Text, Maybe SourceType)]
typeClassIsEmpty :: Bool
typeClassCoveringSets :: Set (Set Int)
typeClassDeterminedArguments :: Set Int
typeClassDependencies :: [FunctionalDependency]
typeClassSuperclasses :: [SourceConstraint]
typeClassMembers :: [(Ident, SourceType)]
typeClassArguments :: [(Text, Maybe SourceType)]
typeClassCoveringSets :: TypeClassData -> Set (Set Int)
typeClassIsEmpty :: TypeClassData -> Bool
typeClassDependencies :: TypeClassData -> [FunctionalDependency]
..} = forall a. a -> Maybe a -> a
fromMaybe (forall a. HasCallStack => String -> a
internalError String
"newDictionaries: type class lookup failed") forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Qualified (ProperName 'ClassName)
className Map (Qualified (ProperName 'ClassName)) TypeClassData
tcs
[NamedDict]
supDicts <- forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\(Constraint (SourceSpan, [Comment])
ann Qualified (ProperName 'ClassName)
supName [SourceType]
supKinds [SourceType]
supArgs Maybe ConstraintData
_) Integer
index ->
let sub :: [(Text, SourceType)]
sub = forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Text, Maybe SourceType)]
typeClassArguments) [SourceType]
instanceTy in
forall (m :: * -> *).
MonadState CheckState m =>
[(Qualified (ProperName 'ClassName), Integer)]
-> Qualified Ident -> SourceConstraint -> m [NamedDict]
newDictionaries ((Qualified (ProperName 'ClassName)
supName, Integer
index) forall a. a -> [a] -> [a]
: [(Qualified (ProperName 'ClassName), Integer)]
path)
Qualified Ident
name
(forall a.
a
-> Qualified (ProperName 'ClassName)
-> [Type a]
-> [Type a]
-> Maybe ConstraintData
-> Constraint a
Constraint (SourceSpan, [Comment])
ann Qualified (ProperName 'ClassName)
supName
(forall a. [(Text, Type a)] -> Type a -> Type a
replaceAllTypeVars [(Text, SourceType)]
sub forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SourceType]
supKinds)
(forall a. [(Text, Type a)] -> Type a -> Type a
replaceAllTypeVars [(Text, SourceType)]
sub forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SourceType]
supArgs)
forall a. Maybe a
Nothing)
) [SourceConstraint]
typeClassSuperclasses [Integer
0..]
forall (m :: * -> *) a. Monad m => a -> m a
return (forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Qualified Ident
name [(Qualified (ProperName 'ClassName), Integer)]
path Qualified (ProperName 'ClassName)
className [] [SourceType]
instanceKinds [SourceType]
instanceTy forall a. Maybe a
Nothing forall a. Maybe a
Nothing forall a. a -> [a] -> [a]
: [NamedDict]
supDicts)
mkContext :: [NamedDict] -> InstanceContext
mkContext :: [NamedDict] -> InstanceContext
mkContext = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr InstanceContext -> InstanceContext -> InstanceContext
combineContexts forall k a. Map k a
M.empty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall {f :: * -> *} {k}.
Applicative f =>
TypeClassDictionaryInScope k
-> Map
QualifiedBy
(Map
(Qualified (ProperName 'ClassName))
(Map k (f (TypeClassDictionaryInScope k))))
fromDict where
fromDict :: TypeClassDictionaryInScope k
-> Map
QualifiedBy
(Map
(Qualified (ProperName 'ClassName))
(Map k (f (TypeClassDictionaryInScope k))))
fromDict TypeClassDictionaryInScope k
d = forall k a. k -> a -> Map k a
M.singleton QualifiedBy
ByNullSourcePos (forall k a. k -> a -> Map k a
M.singleton (forall v.
TypeClassDictionaryInScope v -> Qualified (ProperName 'ClassName)
tcdClassName TypeClassDictionaryInScope k
d) (forall k a. k -> a -> Map k a
M.singleton (forall v. TypeClassDictionaryInScope v -> v
tcdValue TypeClassDictionaryInScope k
d) (forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeClassDictionaryInScope k
d)))
pairwiseAll :: Monoid m => (a -> a -> m) -> [a] -> m
pairwiseAll :: forall m a. Monoid m => (a -> a -> m) -> [a] -> m
pairwiseAll a -> a -> m
_ [] = forall a. Monoid a => a
mempty
pairwiseAll a -> a -> m
_ [a
_] = forall a. Monoid a => a
mempty
pairwiseAll a -> a -> m
p (a
x : [a]
xs) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (a -> a -> m
p a
x) [a]
xs forall a. Semigroup a => a -> a -> a
<> forall m a. Monoid m => (a -> a -> m) -> [a] -> m
pairwiseAll a -> a -> m
p [a]
xs
pairwiseAny :: (a -> a -> Bool) -> [a] -> Bool
pairwiseAny :: forall a. (a -> a -> Bool) -> [a] -> Bool
pairwiseAny a -> a -> Bool
_ [] = Bool
False
pairwiseAny a -> a -> Bool
_ [a
_] = Bool
False
pairwiseAny a -> a -> Bool
p (a
x : [a]
xs) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (a -> a -> Bool
p a
x) [a]
xs Bool -> Bool -> Bool
|| forall a. (a -> a -> Bool) -> [a] -> Bool
pairwiseAny a -> a -> Bool
p [a]
xs
pairwiseM :: Applicative m => (a -> a -> m ()) -> [a] -> m ()
pairwiseM :: forall (m :: * -> *) a.
Applicative m =>
(a -> a -> m ()) -> [a] -> m ()
pairwiseM a -> a -> m ()
_ [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
pairwiseM a -> a -> m ()
_ [a
_] = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
pairwiseM a -> a -> m ()
p (a
x : [a]
xs) = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (a -> a -> m ()
p a
x) [a]
xs forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *) a.
Applicative m =>
(a -> a -> m ()) -> [a] -> m ()
pairwiseM a -> a -> m ()
p [a]
xs
tails1 :: NonEmpty a -> NonEmpty (NonEmpty a)
tails1 :: forall a. NonEmpty a -> NonEmpty (NonEmpty a)
tails1 =
forall a. [a] -> NonEmpty a
NEL.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. [a] -> NonEmpty a
NEL.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
init forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [[a]]
tails forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NonEmpty a -> [a]
NEL.toList