module Language.PureScript.TypeChecker.Entailment
( InstanceContext
, SolverOptions(..)
, replaceTypeClassDictionaries
, newDictionaries
, entails
) where
import Prelude
import Protolude (ordNub)
import Control.Arrow (second, (&&&))
import Control.Monad.Error.Class (MonadError(..))
import Control.Monad.State
import Control.Monad.Supply.Class (MonadSupply(..))
import Control.Monad.Writer
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 qualified Data.Map as M
import qualified Data.Set as S
import Data.Traversable (for)
import Data.Text (Text, stripPrefix, stripSuffix)
import qualified Data.Text as T
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NEL
import Language.PureScript.AST
import Language.PureScript.Crash
import Language.PureScript.Environment
import Language.PureScript.Errors
import Language.PureScript.Names
import Language.PureScript.TypeChecker.Entailment.Coercible
import Language.PureScript.TypeChecker.Entailment.IntCompare
import Language.PureScript.TypeChecker.Kinds (elaborateKind, unifyKinds')
import Language.PureScript.TypeChecker.Monad
import Language.PureScript.TypeChecker.Synonyms (replaceAllTypeSynonyms)
import Language.PureScript.TypeChecker.Unify
import Language.PureScript.TypeClassDictionaries
import Language.PureScript.Types
import Language.PureScript.Label (Label(..))
import Language.PureScript.PSString (PSString, mkString, decodeString)
import qualified Language.PureScript.Constants.Prelude as C
import qualified Language.PureScript.Constants.Prim 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.LT
Ordering
EQ -> Qualified (ProperName 'ConstructorName)
C.EQ
Ordering
GT -> Qualified (ProperName 'ConstructorName)
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)))
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
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)
valUndefined :: Expr
valUndefined :: Expr
valUndefined = SourceSpan -> Qualified Ident -> Expr
Var SourceSpan
nullSourceSpan (forall a. QualifiedBy -> a -> Qualified a
Qualified (ModuleName -> QualifiedBy
ByModuleName ModuleName
C.Prim) (Text -> Ident
Ident forall a. IsString a => a
C.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.orderingLT
Ordering
EQ -> Qualified (ProperName 'TypeName)
C.orderingEQ
Ordering
GT -> Qualified (ProperName 'TypeName)
C.orderingGT
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.booleanTrue -> 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.booleanFalse -> 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.orderingLT -> 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.orderingEQ -> 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.orderingGT -> 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.orderingEQ
Ordering
LT -> Qualified (ProperName 'TypeName)
C.orderingLT
Ordering
GT -> Qualified (ProperName 'TypeName)
C.orderingGT
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.
(Type a -> Type a -> r)
-> Type a
-> Type a
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
alignRowsWith 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.
(Type a -> Type a -> r)
-> Type a
-> Type a
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
alignRowsWith 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