-- |
-- Type class entailment
--
module Language.PureScript.TypeChecker.Entailment
  ( InstanceContext
  , SolverOptions(..)
  , replaceTypeClassDictionaries
  , newDictionaries
  , entails
  , findDicts
  ) where

import Prelude
import Protolude (ordNub)

import Control.Arrow (second, (&&&))
import Control.Monad.Error.Class (MonadError(..))
import Control.Monad.State (MonadState(..), MonadTrans(..), StateT(..), evalStateT, execStateT, foldM, gets, guard, join, modify, zipWithM, zipWithM_, (<=<))
import Control.Monad.Supply.Class (MonadSupply(..))
import Control.Monad.Writer (Any(..), MonadWriter(..), WriterT(..))

import Data.Either (lefts, partitionEithers)
import Data.Foldable (for_, fold, toList)
import Data.Function (on)
import Data.Functor (($>))
import Data.List (delete, findIndices, minimumBy, nubBy, sortOn, tails)
import Data.Maybe (catMaybes, fromMaybe, listToMaybe, mapMaybe)
import Data.Map qualified as M
import Data.Set qualified as S
import Data.Traversable (for)
import Data.Text (Text, stripPrefix, stripSuffix)
import Data.Text qualified as T
import Data.List.NonEmpty (NonEmpty(..))
import Data.List.NonEmpty qualified as NEL

import Language.PureScript.AST (Binder(..), ErrorMessageHint(..), Expr(..), Literal(..), pattern NullSourceSpan, everywhereOnValuesTopDownM, nullSourceSpan)
import Language.PureScript.Crash (internalError)
import Language.PureScript.Environment (Environment(..), FunctionalDependency(..), TypeClassData(..), dictTypeName, kindRow, tyBoolean, tyInt, tyString)
import Language.PureScript.Errors (MultipleErrors, SimpleErrorMessage(..), addHint, addHints, errorMessage, rethrow)
import Language.PureScript.Names (pattern ByNullSourcePos, Ident(..), ModuleName, ProperName(..), ProperNameType(..), Qualified(..), QualifiedBy(..), byMaybeModuleName, coerceProperName, disqualify, freshIdent, getQual)
import Language.PureScript.TypeChecker.Entailment.Coercible (GivenSolverState(..), WantedSolverState(..), initialGivenSolverState, initialWantedSolverState, insoluble, solveGivens, solveWanteds)
import Language.PureScript.TypeChecker.Entailment.IntCompare (mkFacts, mkRelation, solveRelation)
import Language.PureScript.TypeChecker.Kinds (elaborateKind, unifyKinds')
import Language.PureScript.TypeChecker.Monad (CheckState(..), withErrorMessageHint)
import Language.PureScript.TypeChecker.Synonyms (replaceAllTypeSynonyms)
import Language.PureScript.TypeChecker.Unify (freshTypeWithKind, substituteType, unifyTypes)
import Language.PureScript.TypeClassDictionaries (NamedDict, TypeClassDictionaryInScope(..), superclassName)
import Language.PureScript.Types
import Language.PureScript.Label (Label(..))
import Language.PureScript.PSString (PSString, mkString, decodeString)
import Language.PureScript.Constants.Libs qualified as C
import Language.PureScript.Constants.Prim qualified as C

-- | Describes what sort of dictionary to generate for type class instances
data Evidence
  -- | An existing named instance
  = NamedInstance (Qualified Ident)

  -- | Computed instances
  | WarnInstance SourceType -- ^ Warn type class with a user-defined warning message
  | IsSymbolInstance PSString -- ^ The IsSymbol type class for a given Symbol literal
  | ReflectableInstance Reflectable -- ^ The Reflectable type class for a reflectable kind
  | EmptyClassInstance        -- ^ For any solved type class with no members
  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)

-- | Describes kinds that are reflectable to the term-level
data Reflectable
  = ReflectableInt Integer -- ^ For type-level numbers
  | ReflectableString PSString -- ^ For type-level strings
  | ReflectableBoolean Bool -- ^ For type-level booleans
  | ReflectableOrdering Ordering -- ^ For type-level orderings
  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)

-- | Reflect a reflectable type into an expression
asExpression :: Reflectable -> Expr
asExpression :: Reflectable -> Expr
asExpression = \case
  ReflectableInt Integer
n -> SourceSpan -> Literal Expr -> Expr
Literal SourceSpan
NullSourceSpan forall a b. (a -> b) -> a -> b
$ forall a. Either Integer Double -> Literal a
NumericLiteral forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left Integer
n
  ReflectableString PSString
s -> SourceSpan -> Literal Expr -> Expr
Literal SourceSpan
NullSourceSpan forall a b. (a -> b) -> a -> b
$ forall a. PSString -> Literal a
StringLiteral PSString
s
  ReflectableBoolean Bool
b -> SourceSpan -> Literal Expr -> Expr
Literal SourceSpan
NullSourceSpan forall a b. (a -> b) -> a -> b
$ forall a. Bool -> Literal a
BooleanLiteral Bool
b
  ReflectableOrdering Ordering
o -> SourceSpan -> Qualified (ProperName 'ConstructorName) -> Expr
Constructor SourceSpan
NullSourceSpan forall a b. (a -> b) -> a -> b
$ case Ordering
o of
    Ordering
LT -> Qualified (ProperName 'ConstructorName)
C.C_LT
    Ordering
EQ -> Qualified (ProperName 'ConstructorName)
C.C_EQ
    Ordering
GT -> Qualified (ProperName 'ConstructorName)
C.C_GT

-- | Extract the identifier of a named instance
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

-- | Description of a type class dictionary with instance evidence
type TypeClassDict = TypeClassDictionaryInScope Evidence

-- | The 'InstanceContext' tracks those constraints which can be satisfied.
type InstanceContext = M.Map QualifiedBy
                         (M.Map (Qualified (ProperName 'ClassName))
                           (M.Map (Qualified Ident) (NonEmpty NamedDict)))

findDicts :: InstanceContext -> Qualified (ProperName 'ClassName) -> QualifiedBy -> [TypeClassDict]
findDicts :: InstanceContext
-> Qualified (ProperName 'ClassName)
-> QualifiedBy
-> [TypeClassDict]
findDicts InstanceContext
ctx Qualified (ProperName 'ClassName)
cn = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Qualified Ident -> Evidence
NamedInstance) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. NonEmpty a -> [a]
NEL.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall k a. Map k a -> [a]
M.elems forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Qualified (ProperName 'ClassName)
cn forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall a b c. (a -> b -> c) -> b -> a -> c
flip forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup InstanceContext
ctx)

-- | A type substitution which makes an instance head match a list of types.
--
-- Note: we store many types per type variable name. For any name, all types
-- should unify if we are going to commit to an instance.
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
(<>)))

-- | Replace type class dictionary placeholders with inferred type class dictionaries
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
    -- Loop, deferring any unsolved constraints, until there are no more
    -- constraints which can be solved, then make a generalization pass.
    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
    -- This pass solves constraints where possible, deferring constraints if not.
    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

    -- This pass generalizes any remaining constraints
    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

-- | Three options for how we can handle a constraint, depending on the mode we're in.
data EntailsResult a
  = Solved a TypeClassDict
  -- ^ We solved this constraint
  | Unsolved SourceConstraint
  -- ^ We couldn't solve this constraint right now, it will be generalized
  | Deferred
  -- ^ We couldn't solve this constraint right now, so it has been 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

-- | Options for the constraint solver
data SolverOptions = SolverOptions
  { SolverOptions -> Bool
solverShouldGeneralize :: Bool
  -- ^ Should the solver be allowed to generalize over unsolved constraints?
  , SolverOptions -> Bool
solverDeferErrors      :: Bool
  -- ^ Should the solver be allowed to defer errors by skipping constraints?
  }

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

-- | Check that the current set of type class dictionaries entail the specified type class goal, and, if so,
-- return a type class dictionary reference.
entails
  :: forall m
   . (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m, MonadSupply m)
  => SolverOptions
  -- ^ Solver options
  -> SourceConstraint
  -- ^ The constraint to solve
  -> InstanceContext
  -- ^ The contexts in which to solve the constraint
  -> [ErrorMessageHint]
  -- ^ Error message hints to apply to any instance errors
  -> 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] =
      -- Prefer a warning dictionary in scope if there is one available.
      -- This allows us to defer a warning by propagating the constraint.
      InstanceContext
-> Qualified (ProperName 'ClassName)
-> QualifiedBy
-> [TypeClassDict]
findDicts InstanceContext
ctx Qualified (ProperName 'ClassName)
cn QualifiedBy
ByNullSourcePos forall a. [a] -> [a] -> [a]
++ [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 (SourceType -> Evidence
WarnInstance SourceType
msg) [] Qualified (ProperName 'ClassName)
C.Warn [] [] [SourceType
msg] forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
    forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.IsSymbol [SourceType]
_ [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> Maybe [TypeClassDict]
solveIsSymbol [SourceType]
args = [TypeClassDict]
dicts
    forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.SymbolCompare [SourceType]
_ [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> Maybe [TypeClassDict]
solveSymbolCompare [SourceType]
args = [TypeClassDict]
dicts
    forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.SymbolAppend [SourceType]
_ [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> Maybe [TypeClassDict]
solveSymbolAppend [SourceType]
args = [TypeClassDict]
dicts
    forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.SymbolCons [SourceType]
_ [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> Maybe [TypeClassDict]
solveSymbolCons [SourceType]
args = [TypeClassDict]
dicts
    forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.IntAdd [SourceType]
_ [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> Maybe [TypeClassDict]
solveIntAdd [SourceType]
args = [TypeClassDict]
dicts
    forClassName Environment
_ InstanceContext
ctx Qualified (ProperName 'ClassName)
C.IntCompare [SourceType]
_ [SourceType]
args | Just [TypeClassDict]
dicts <- InstanceContext -> [SourceType] -> Maybe [TypeClassDict]
solveIntCompare InstanceContext
ctx [SourceType]
args = [TypeClassDict]
dicts
    forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.IntMul [SourceType]
_ [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> Maybe [TypeClassDict]
solveIntMul [SourceType]
args = [TypeClassDict]
dicts
    forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.IntToString [SourceType]
_ [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> Maybe [TypeClassDict]
solveIntToString [SourceType]
args = [TypeClassDict]
dicts
    forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.Reflectable [SourceType]
_ [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> Maybe [TypeClassDict]
solveReflectable [SourceType]
args = [TypeClassDict]
dicts
    forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.RowUnion [SourceType]
kinds [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
solveUnion [SourceType]
kinds [SourceType]
args = [TypeClassDict]
dicts
    forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.RowNub [SourceType]
kinds [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
solveNub [SourceType]
kinds [SourceType]
args = [TypeClassDict]
dicts
    forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.RowLacks [SourceType]
kinds [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
solveLacks [SourceType]
kinds [SourceType]
args = [TypeClassDict]
dicts
    forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.RowCons [SourceType]
kinds [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
solveRowCons [SourceType]
kinds [SourceType]
args = [TypeClassDict]
dicts
    forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
C.RowToList [SourceType]
kinds [SourceType]
args | Just [TypeClassDict]
dicts <- [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
solveRowToList [SourceType]
kinds [SourceType]
args = [TypeClassDict]
dicts
    forClassName Environment
_ InstanceContext
ctx cn :: Qualified (ProperName 'ClassName)
cn@(Qualified (ByModuleName ModuleName
mn) ProperName 'ClassName
_) [SourceType]
_ [SourceType]
tys = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (InstanceContext
-> Qualified (ProperName 'ClassName)
-> QualifiedBy
-> [TypeClassDict]
findDicts InstanceContext
ctx Qualified (ProperName 'ClassName)
cn) (forall a. Ord a => [a] -> [a]
ordNub (QualifiedBy
ByNullSourcePos forall a. a -> [a] -> [a]
: ModuleName -> QualifiedBy
ByModuleName ModuleName
mn forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map ModuleName -> QualifiedBy
ByModuleName (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe SourceType -> Maybe ModuleName
ctorModules [SourceType]
tys)))
    forClassName Environment
_ InstanceContext
_ Qualified (ProperName 'ClassName)
_ [SourceType]
_ [SourceType]
_ = forall a. HasCallStack => String -> a
internalError String
"forClassName: expected qualified class name"

    ctorModules :: SourceType -> Maybe ModuleName
    ctorModules :: SourceType -> Maybe ModuleName
ctorModules (TypeConstructor (SourceSpan, [Comment])
_ (Qualified (ByModuleName ModuleName
mn) ProperName 'TypeName
_)) = forall a. a -> Maybe a
Just ModuleName
mn
    ctorModules (TypeConstructor (SourceSpan, [Comment])
_ (Qualified (BySourcePos SourcePos
_) ProperName 'TypeName
_)) = forall a. HasCallStack => String -> a
internalError String
"ctorModules: unqualified type name"
    ctorModules (TypeApp (SourceSpan, [Comment])
_ SourceType
ty SourceType
_) = SourceType -> Maybe ModuleName
ctorModules SourceType
ty
    ctorModules (KindApp (SourceSpan, [Comment])
_ SourceType
ty SourceType
_) = SourceType -> Maybe ModuleName
ctorModules SourceType
ty
    ctorModules (KindedType (SourceSpan, [Comment])
_ SourceType
ty SourceType
_) = SourceType -> Maybe ModuleName
ctorModules SourceType
ty
    ctorModules SourceType
_ = forall a. Maybe a
Nothing

    valUndefined :: Expr
    valUndefined :: Expr
valUndefined = SourceSpan -> Qualified Ident -> Expr
Var SourceSpan
nullSourceSpan Qualified Ident
C.I_undefined

    solve :: SourceConstraint -> WriterT (Any, [(Ident, InstanceContext, SourceConstraint)]) (StateT InstanceContext m) Expr
    solve :: SourceConstraint
-> WriterT
     (Any, [(Ident, InstanceContext, SourceConstraint)])
     (StateT InstanceContext m)
     Expr
solve = Int
-> [ErrorMessageHint]
-> SourceConstraint
-> WriterT
     (Any, [(Ident, InstanceContext, SourceConstraint)])
     (StateT InstanceContext m)
     Expr
go Int
0 [ErrorMessageHint]
hints
      where
        go :: Int -> [ErrorMessageHint] -> SourceConstraint -> WriterT (Any, [(Ident, InstanceContext, SourceConstraint)]) (StateT InstanceContext m) Expr
        go :: Int
-> [ErrorMessageHint]
-> SourceConstraint
-> WriterT
     (Any, [(Ident, InstanceContext, SourceConstraint)])
     (StateT InstanceContext m)
     Expr
go Int
work [ErrorMessageHint]
_ (Constraint (SourceSpan, [Comment])
_ Qualified (ProperName 'ClassName)
className' [SourceType]
_ [SourceType]
tys' Maybe ConstraintData
_) | Int
work forall a. Ord a => a -> a -> Bool
> Int
1000 = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleErrorMessage -> MultipleErrors
errorMessage forall a b. (a -> b) -> a -> b
$ Qualified (ProperName 'ClassName)
-> [SourceType] -> SimpleErrorMessage
PossiblyInfiniteInstance Qualified (ProperName 'ClassName)
className' [SourceType]
tys'
        go Int
work [ErrorMessageHint]
hints' con :: SourceConstraint
con@(Constraint (SourceSpan, [Comment])
_ Qualified (ProperName 'ClassName)
className' [SourceType]
kinds' [SourceType]
tys' Maybe ConstraintData
conInfo) = forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m) =>
ErrorMessageHint -> m a -> m a
withErrorMessageHint (SourceConstraint -> ErrorMessageHint
ErrorSolvingConstraint SourceConstraint
con) forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT forall a b. (a -> b) -> a -> b
$ do
            -- We might have unified types by solving other constraints, so we need to
            -- apply the latest substitution.
            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'

            -- Get the inferred constraint context so far, and merge it with the global context
            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
            -- We need information about functional dependencies, so we have to look up the class
            -- name in the environment:
            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
                  -- process instances in a chain in index order
                  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) ->
                                -- Make sure the type unifies with the type in the type instance definition
                                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 ()                   -- keep searching
                                  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)) -- found a match
                                  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 ()                                   -- need proof of apartness but this is either not in a chain or at the end
                                    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)) -- can't continue with this chain yet, need proof of apartness

                  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
                -- Note that we solved something.
                forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Bool -> Any
Any Bool
True, forall a. Monoid a => a
mempty)
                -- Make sure the substitution is valid:
                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
                -- Now enforce any functional dependencies, using unification
                -- Note: we need to generate fresh types for any unconstrained
                -- type variables before unifying.
                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'
                -- Solve any necessary subgoals
                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
                -- Generate a fresh name for the unsolved constraint's new dictionary
                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
                -- Store the new dictionary in the InstanceContext so that we can solve this goal in
                -- future.
                [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)
                -- Mark this constraint for generalization
                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 ->
                -- Constraint was deferred, just return the dictionary unchanged,
                -- with no unsolved constraints. Hopefully, we can solve this later.
                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
            -- When checking functional dependencies, we need to use unification to make
            -- sure it is safe to use the selected instance. We will unify the solved type with
            -- the type in the instance head under the substitution inferred from its instantiation.
            -- As an example, when solving MonadState t0 (State Int), we choose the
            -- MonadState s (State s) instance, and we unify t0 with Int, since the functional
            -- dependency from MonadState dictates that t0 should unify with s\[s -> Int], which is
            -- Int. This is fine, but in some cases, the substitution does not remove all TypeVars
            -- from the type, so we end up with a unification error. So, any type arguments which
            -- appear in the instance head, but not in the substitution need to be replaced with
            -- fresh type variables. This function extends a substitution with fresh type variables
            -- as necessary, based on the types in the instance head. It also unifies kinds based on
            -- the substitution so kind information propagates correctly through the solver.
            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
              -- We need a special case for nullary type classes, since we want
              -- to generalize over Partial constraints.
              | 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

            -- Check if two dictionaries are overlapping
            --
            -- Dictionaries which are subclass dictionaries cannot overlap, since otherwise the overlap would have
            -- been caught when constructing superclass dictionaries.
            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

            -- Create dictionaries for subgoals which still need to be solved by calling go recursively
            -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type
            -- unifies with Either a b, and we can satisfy the subgoals Show a and Show b recursively.
            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

            -- We need subgoal dictionaries to appear in the term somewhere
            -- If there aren't any then the dictionary is just undefined
            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))

            -- Make a dictionary from subgoal dictionaries by applying the correct function
            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
              -- We cannot call the type class constructor here because Warn is declared in Prim.
              -- This means that it doesn't have a definition that we can import.
              -- So pass an empty placeholder (undefined) instead.
              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

        -- Turn a DictionaryValue into a Expr
        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
      -- Solving fails when there's irreducible wanteds left.
      --
      -- We report the first residual constraint instead of the initial wanted,
      -- unless we just swapped its arguments.
      --
      -- We may have collected hints for the solving failure along the way, in
      -- which case we decorate the error with the first one.
      forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id ErrorMessageHint -> MultipleErrors -> MultipleErrors
addHint (forall a. [a] -> Maybe a
listToMaybe [ErrorMessageHint]
hints') forall e (m :: * -> *) a. MonadError e m => (e -> e) -> m a -> m a
`rethrow` case [(SourceType, SourceType, SourceType)]
inertWanteds of
        [] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.Coercible [] [SourceType]
kinds [SourceType
a, SourceType
b] forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
        (SourceType
k, SourceType
a', SourceType
b') : [(SourceType, SourceType, SourceType)]
_ | SourceType
a' forall a. Eq a => a -> a -> Bool
== SourceType
b Bool -> Bool -> Bool
&& SourceType
b' forall a. Eq a => a -> a -> Bool
== SourceType
a -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType -> SourceType -> MultipleErrors
insoluble SourceType
k SourceType
b' SourceType
a'
        (SourceType
k, SourceType
a', SourceType
b') : [(SourceType, SourceType, SourceType)]
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ SourceType -> SourceType -> SourceType -> MultipleErrors
insoluble SourceType
k SourceType
a' SourceType
b'
    solveCoercible Environment
_ InstanceContext
_ [SourceType]
_ [SourceType]
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing

    solveIsSymbol :: [SourceType] -> Maybe [TypeClassDict]
    solveIsSymbol :: [SourceType] -> Maybe [TypeClassDict]
solveIsSymbol [TypeLevelString (SourceSpan, [Comment])
ann PSString
sym] = forall a. a -> Maybe a
Just [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 (PSString -> Evidence
IsSymbolInstance PSString
sym) [] Qualified (ProperName 'ClassName)
C.IsSymbol [] [] [forall a. a -> PSString -> Type a
TypeLevelString (SourceSpan, [Comment])
ann PSString
sym] forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
    solveIsSymbol [SourceType]
_ = forall a. Maybe a
Nothing

    solveSymbolCompare :: [SourceType] -> Maybe [TypeClassDict]
    solveSymbolCompare :: [SourceType] -> Maybe [TypeClassDict]
solveSymbolCompare [arg0 :: SourceType
arg0@(TypeLevelString (SourceSpan, [Comment])
_ PSString
lhs), arg1 :: SourceType
arg1@(TypeLevelString (SourceSpan, [Comment])
_ PSString
rhs), SourceType
_] =
      let ordering :: Qualified (ProperName 'TypeName)
ordering = case forall a. Ord a => a -> a -> Ordering
compare PSString
lhs PSString
rhs of
                  Ordering
LT -> Qualified (ProperName 'TypeName)
C.LT
                  Ordering
EQ -> Qualified (ProperName 'TypeName)
C.EQ
                  Ordering
GT -> Qualified (ProperName 'TypeName)
C.GT
          args' :: [SourceType]
args' = [SourceType
arg0, SourceType
arg1, Qualified (ProperName 'TypeName) -> SourceType
srcTypeConstructor Qualified (ProperName 'TypeName)
ordering]
      in forall a. a -> Maybe a
Just [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.SymbolCompare [] [] [SourceType]
args' forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
    solveSymbolCompare [SourceType]
_ = forall a. Maybe a
Nothing

    solveSymbolAppend :: [SourceType] -> Maybe [TypeClassDict]
    solveSymbolAppend :: [SourceType] -> Maybe [TypeClassDict]
solveSymbolAppend [SourceType
arg0, SourceType
arg1, SourceType
arg2] = do
      (SourceType
arg0', SourceType
arg1', SourceType
arg2') <- SourceType
-> SourceType
-> SourceType
-> Maybe (SourceType, SourceType, SourceType)
appendSymbols SourceType
arg0 SourceType
arg1 SourceType
arg2
      let args' :: [SourceType]
args' = [SourceType
arg0', SourceType
arg1', SourceType
arg2']
      forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.SymbolAppend [] [] [SourceType]
args' forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
    solveSymbolAppend [SourceType]
_ = forall a. Maybe a
Nothing

    -- Append type level symbols, or, run backwards, strip a prefix or suffix
    appendSymbols :: SourceType -> SourceType -> SourceType -> Maybe (SourceType, SourceType, SourceType)
    appendSymbols :: SourceType
-> SourceType
-> SourceType
-> Maybe (SourceType, SourceType, SourceType)
appendSymbols arg0 :: SourceType
arg0@(TypeLevelString (SourceSpan, [Comment])
_ PSString
lhs) arg1 :: SourceType
arg1@(TypeLevelString (SourceSpan, [Comment])
_ PSString
rhs) SourceType
_ = forall a. a -> Maybe a
Just (SourceType
arg0, SourceType
arg1, PSString -> SourceType
srcTypeLevelString (PSString
lhs forall a. Semigroup a => a -> a -> a
<> PSString
rhs))
    appendSymbols arg0 :: SourceType
arg0@(TypeLevelString (SourceSpan, [Comment])
_ PSString
lhs) SourceType
_ arg2 :: SourceType
arg2@(TypeLevelString (SourceSpan, [Comment])
_ PSString
out) = do
      Text
lhs' <- PSString -> Maybe Text
decodeString PSString
lhs
      Text
out' <- PSString -> Maybe Text
decodeString PSString
out
      Text
rhs <- Text -> Text -> Maybe Text
stripPrefix Text
lhs' Text
out'
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
arg0, PSString -> SourceType
srcTypeLevelString (Text -> PSString
mkString Text
rhs), SourceType
arg2)
    appendSymbols SourceType
_ arg1 :: SourceType
arg1@(TypeLevelString (SourceSpan, [Comment])
_ PSString
rhs) arg2 :: SourceType
arg2@(TypeLevelString (SourceSpan, [Comment])
_ PSString
out) = do
      Text
rhs' <- PSString -> Maybe Text
decodeString PSString
rhs
      Text
out' <- PSString -> Maybe Text
decodeString PSString
out
      Text
lhs <- Text -> Text -> Maybe Text
stripSuffix Text
rhs' Text
out'
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (PSString -> SourceType
srcTypeLevelString (Text -> PSString
mkString Text
lhs), SourceType
arg1, SourceType
arg2)
    appendSymbols SourceType
_ SourceType
_ SourceType
_ = forall a. Maybe a
Nothing

    solveSymbolCons :: [SourceType] -> Maybe [TypeClassDict]
    solveSymbolCons :: [SourceType] -> Maybe [TypeClassDict]
solveSymbolCons [SourceType
arg0, SourceType
arg1, SourceType
arg2] = do
      (SourceType
arg0', SourceType
arg1', SourceType
arg2') <- SourceType
-> SourceType
-> SourceType
-> Maybe (SourceType, SourceType, SourceType)
consSymbol SourceType
arg0 SourceType
arg1 SourceType
arg2
      let args' :: [SourceType]
args' = [SourceType
arg0', SourceType
arg1', SourceType
arg2']
      forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.SymbolCons [] [] [SourceType]
args' forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
    solveSymbolCons [SourceType]
_ = forall a. Maybe a
Nothing

    consSymbol :: SourceType -> SourceType -> SourceType -> Maybe (SourceType, SourceType, SourceType)
    consSymbol :: SourceType
-> SourceType
-> SourceType
-> Maybe (SourceType, SourceType, SourceType)
consSymbol SourceType
_ SourceType
_ arg :: SourceType
arg@(TypeLevelString (SourceSpan, [Comment])
_ PSString
s) = do
      (Char
h, Text
t) <- Text -> Maybe (Char, Text)
T.uncons forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< PSString -> Maybe Text
decodeString PSString
s
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> SourceType
mkTLString (Char -> Text
T.singleton Char
h), Text -> SourceType
mkTLString Text
t, SourceType
arg)
      where mkTLString :: Text -> SourceType
mkTLString = PSString -> SourceType
srcTypeLevelString forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> PSString
mkString
    consSymbol arg1 :: SourceType
arg1@(TypeLevelString (SourceSpan, [Comment])
_ PSString
h) arg2 :: SourceType
arg2@(TypeLevelString (SourceSpan, [Comment])
_ PSString
t) SourceType
_ = do
      Text
h' <- PSString -> Maybe Text
decodeString PSString
h
      Text
t' <- PSString -> Maybe Text
decodeString PSString
t
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Text -> Int
T.length Text
h' forall a. Eq a => a -> a -> Bool
== Int
1)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
arg1, SourceType
arg2, PSString -> SourceType
srcTypeLevelString (Text -> PSString
mkString forall a b. (a -> b) -> a -> b
$ Text
h' forall a. Semigroup a => a -> a -> a
<> Text
t'))
    consSymbol SourceType
_ SourceType
_ SourceType
_ = forall a. Maybe a
Nothing

    solveIntToString :: [SourceType] -> Maybe [TypeClassDict]
    solveIntToString :: [SourceType] -> Maybe [TypeClassDict]
solveIntToString [SourceType
arg0, SourceType
_] = do
      (SourceType
arg0', SourceType
arg1') <- SourceType -> Maybe (SourceType, SourceType)
printIntToString SourceType
arg0
      let args' :: [SourceType]
args' = [SourceType
arg0', SourceType
arg1']
      forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.IntToString [] [] [SourceType]
args' forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
    solveIntToString [SourceType]
_ = forall a. Maybe a
Nothing

    printIntToString :: SourceType -> Maybe (SourceType, SourceType)
    printIntToString :: SourceType -> Maybe (SourceType, SourceType)
printIntToString arg0 :: SourceType
arg0@(TypeLevelInt (SourceSpan, [Comment])
_ Integer
i) = do
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourceType
arg0, PSString -> SourceType
srcTypeLevelString forall a b. (a -> b) -> a -> b
$ Text -> PSString
mkString forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Integer
i)
    printIntToString SourceType
_ = forall a. Maybe a
Nothing

    solveReflectable :: [SourceType] -> Maybe [TypeClassDict]
    solveReflectable :: [SourceType] -> Maybe [TypeClassDict]
solveReflectable [SourceType
typeLevel, SourceType
_] = do
      (Reflectable
ref, SourceType
typ) <- case SourceType
typeLevel of
        TypeLevelInt (SourceSpan, [Comment])
_ Integer
i -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Reflectable
ReflectableInt Integer
i, SourceType
tyInt)
        TypeLevelString (SourceSpan, [Comment])
_ PSString
s -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (PSString -> Reflectable
ReflectableString PSString
s, SourceType
tyString)
        TypeConstructor (SourceSpan, [Comment])
_ Qualified (ProperName 'TypeName)
n
          | Qualified (ProperName 'TypeName)
n forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'TypeName)
C.True -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Reflectable
ReflectableBoolean Bool
True, SourceType
tyBoolean)
          | Qualified (ProperName 'TypeName)
n forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'TypeName)
C.False -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Reflectable
ReflectableBoolean Bool
False, SourceType
tyBoolean)
          | Qualified (ProperName 'TypeName)
n forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'TypeName)
C.LT -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ordering -> Reflectable
ReflectableOrdering Ordering
LT, Qualified (ProperName 'TypeName) -> SourceType
srcTypeConstructor Qualified (ProperName 'TypeName)
C.Ordering)
          | Qualified (ProperName 'TypeName)
n forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'TypeName)
C.EQ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ordering -> Reflectable
ReflectableOrdering Ordering
EQ, Qualified (ProperName 'TypeName) -> SourceType
srcTypeConstructor Qualified (ProperName 'TypeName)
C.Ordering)
          | Qualified (ProperName 'TypeName)
n forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'TypeName)
C.GT -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ordering -> Reflectable
ReflectableOrdering Ordering
GT, Qualified (ProperName 'TypeName) -> SourceType
srcTypeConstructor Qualified (ProperName 'TypeName)
C.Ordering)
        SourceType
_ -> forall a. Maybe a
Nothing
      forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 (Reflectable -> Evidence
ReflectableInstance Reflectable
ref) [] Qualified (ProperName 'ClassName)
C.Reflectable [] [] [SourceType
typeLevel, SourceType
typ] forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
    solveReflectable [SourceType]
_ = forall a. Maybe a
Nothing

    solveIntAdd :: [SourceType] -> Maybe [TypeClassDict]
    solveIntAdd :: [SourceType] -> Maybe [TypeClassDict]
solveIntAdd [SourceType
arg0, SourceType
arg1, SourceType
arg2] = do
      (SourceType
arg0', SourceType
arg1', SourceType
arg2') <- SourceType
-> SourceType
-> SourceType
-> Maybe (SourceType, SourceType, SourceType)
addInts SourceType
arg0 SourceType
arg1 SourceType
arg2
      let args' :: [SourceType]
args' = [SourceType
arg0', SourceType
arg1', SourceType
arg2']
      forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.IntAdd [] [] [SourceType]
args' forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
    solveIntAdd [SourceType]
_ = forall a. Maybe a
Nothing

    addInts :: SourceType -> SourceType -> SourceType -> Maybe (SourceType, SourceType, SourceType)
    -- l r -> o, l + r = o
    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))
    -- l o -> r, o - l = 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)
    -- r o -> l, o - r = l
    addInts SourceType
_ arg1 :: SourceType
arg1@(TypeLevelInt (SourceSpan, [Comment])
_ Integer
r) arg2 :: SourceType
arg2@(TypeLevelInt (SourceSpan, [Comment])
_ Integer
o) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SourceType
srcTypeLevelInt (Integer
o forall a. Num a => a -> a -> a
- Integer
r), SourceType
arg1, SourceType
arg2)
    addInts SourceType
_ SourceType
_ SourceType
_                                             = forall a. Maybe a
Nothing

    solveIntCompare :: InstanceContext -> [SourceType] -> Maybe [TypeClassDict]
    solveIntCompare :: InstanceContext -> [SourceType] -> Maybe [TypeClassDict]
solveIntCompare InstanceContext
_ [arg0 :: SourceType
arg0@(TypeLevelInt (SourceSpan, [Comment])
_ Integer
a), arg1 :: SourceType
arg1@(TypeLevelInt (SourceSpan, [Comment])
_ Integer
b), SourceType
_] =
      let ordering :: Qualified (ProperName 'TypeName)
ordering = case forall a. Ord a => a -> a -> Ordering
compare Integer
a Integer
b of
            Ordering
EQ -> Qualified (ProperName 'TypeName)
C.EQ
            Ordering
LT -> Qualified (ProperName 'TypeName)
C.LT
            Ordering
GT -> Qualified (ProperName 'TypeName)
C.GT
          args' :: [SourceType]
args' = [SourceType
arg0, SourceType
arg1, Qualified (ProperName 'TypeName) -> SourceType
srcTypeConstructor Qualified (ProperName 'TypeName)
ordering]
      in forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.IntCompare [] [] [SourceType]
args' forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
    solveIntCompare InstanceContext
ctx args :: [SourceType]
args@[SourceType
a, SourceType
b, SourceType
_] = do
      let compareDictsInScope :: [TypeClassDict]
compareDictsInScope = InstanceContext
-> Qualified (ProperName 'ClassName)
-> QualifiedBy
-> [TypeClassDict]
findDicts InstanceContext
ctx Qualified (ProperName 'ClassName)
C.IntCompare QualifiedBy
ByNullSourcePos
          givens :: Context SourceType
givens = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe [TypeClassDict]
compareDictsInScope forall a b. (a -> b) -> a -> b
$ \case
            TypeClassDict
dict | [SourceType
a', SourceType
b', SourceType
c'] <- forall v. TypeClassDictionaryInScope v -> [SourceType]
tcdInstanceTypes TypeClassDict
dict -> forall a. Type a -> Type a -> Type a -> Maybe (Relation (Type a))
mkRelation SourceType
a' SourceType
b' SourceType
c'
                 | Bool
otherwise -> forall a. Maybe a
Nothing
          facts :: Context SourceType
facts = forall a. [[Type a]] -> [Relation (Type a)]
mkFacts ([SourceType]
args forall a. a -> [a] -> [a]
: (forall v. TypeClassDictionaryInScope v -> [SourceType]
tcdInstanceTypes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TypeClassDict]
compareDictsInScope))
      Qualified (ProperName 'TypeName)
c' <- forall a.
Ord a =>
Context a -> a -> a -> Maybe (Qualified (ProperName 'TypeName))
solveRelation (Context SourceType
givens forall a. Semigroup a => a -> a -> a
<> Context SourceType
facts) SourceType
a SourceType
b
      forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.IntCompare [] [] [SourceType
a, SourceType
b, Qualified (ProperName 'TypeName) -> SourceType
srcTypeConstructor Qualified (ProperName 'TypeName)
c'] forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
    solveIntCompare InstanceContext
_ [SourceType]
_ = forall a. Maybe a
Nothing

    solveIntMul :: [SourceType] -> Maybe [TypeClassDict]
    solveIntMul :: [SourceType] -> Maybe [TypeClassDict]
solveIntMul [arg0 :: SourceType
arg0@(TypeLevelInt (SourceSpan, [Comment])
_ Integer
l), arg1 :: SourceType
arg1@(TypeLevelInt (SourceSpan, [Comment])
_ Integer
r), SourceType
_] =
      let args' :: [SourceType]
args' = [SourceType
arg0, SourceType
arg1, Integer -> SourceType
srcTypeLevelInt (Integer
l forall a. Num a => a -> a -> a
* Integer
r)]
      in forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.IntMul [] [] [SourceType]
args' forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
    solveIntMul [SourceType]
_ = forall a. Maybe a
Nothing

    solveUnion :: [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
    solveUnion :: [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
solveUnion [SourceType]
kinds [SourceType
l, SourceType
r, SourceType
u] = do
      (SourceType
lOut, SourceType
rOut, SourceType
uOut, Maybe [SourceConstraint]
cst, [(Text, SourceType)]
vars) <- [SourceType]
-> SourceType
-> SourceType
-> SourceType
-> Maybe
     (SourceType, SourceType, SourceType, Maybe [SourceConstraint],
      [(Text, SourceType)])
unionRows [SourceType]
kinds SourceType
l SourceType
r SourceType
u
      forall (f :: * -> *) a. Applicative f => a -> f a
pure [ forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.RowUnion [(Text, SourceType)]
vars [SourceType]
kinds [SourceType
lOut, SourceType
rOut, SourceType
uOut] Maybe [SourceConstraint]
cst forall a. Maybe a
Nothing ]
    solveUnion [SourceType]
_ [SourceType]
_ = forall a. Maybe a
Nothing

    -- Left biased union of two row types

    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
            -- If the left hand side is a closed row, then we can merge
            -- its labels into the right hand side.
            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, [])
            -- If the right hand side and output are closed rows, then we can
            -- compute the left hand side by subtracting the right hand side
            -- from the output.
            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
                -- Partition the output rows into those that belong in right
                -- (taken off the end) and those that must end up in left.
                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
                 , []
                 )
            -- If the left hand side is not definitely closed, then the only way we
            -- can safely make progress is to move any known labels from the left
            -- input into the output, and add a constraint for any remaining labels.
            -- Otherwise, the left hand tail might contain the same labels as on
            -- the right hand side, and we can't be certain we won't reorder the
            -- types for such labels.
            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

    -- Convert a closed row to a sorted list of entries
    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 ])

-- Check if an instance matches our list of types, allowing for types
-- to be solved via functional dependencies. If the types match, we return a
-- substitution which makes them match. If not, we return '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 =
    -- First, find those types which match exactly
    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
    -- Now, use any functional dependencies to infer any remaining types
    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 -- Verify that any repeated type variables are unifiable
            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
    -- Find the closure of a set of functional dependencies.
    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

    --
    -- Check whether the type heads of two types are equal (for the purposes of type class dictionary lookup),
    -- and return a substitution from type variables to types which makes the type heads unify.
    --
    typeHeadsAreEqual :: Type a -> Type a -> (Matched (), Matching [Type a])
    typeHeadsAreEqual :: forall a. Type a -> Type a -> (Matched (), Matching [Type a])
typeHeadsAreEqual (KindedType a
_  Type a
t1 Type a
_) Type a
t2                                  = forall a. Type a -> Type a -> (Matched (), Matching [Type a])
typeHeadsAreEqual Type a
t1 Type a
t2
    typeHeadsAreEqual Type a
t1                     (KindedType a
_ Type a
t2 Type a
_)               = forall a. Type a -> Type a -> (Matched (), Matching [Type a])
typeHeadsAreEqual Type a
t1 Type a
t2
    typeHeadsAreEqual (TUnknown a
_ Int
u1)        (TUnknown a
_ Int
u2)      | Int
u1 forall a. Eq a => a -> a -> Bool
== Int
u2   = (forall t. t -> Matched t
Match (), forall k a. Map k a
M.empty)
    typeHeadsAreEqual (Skolem a
_ Text
_ Maybe (Type a)
_ Int
s1 SkolemScope
_)      (Skolem a
_ Text
_ Maybe (Type a)
_ Int
s2 SkolemScope
_)    | Int
s1 forall a. Eq a => a -> a -> Bool
== Int
s2   = (forall t. t -> Matched t
Match (), forall k a. Map k a
M.empty)
    typeHeadsAreEqual Type a
t                      (TypeVar a
_ Text
v)                     = (forall t. t -> Matched t
Match (), forall k a. k -> a -> Map k a
M.singleton Text
v [Type a
t])
    typeHeadsAreEqual (TypeConstructor a
_ Qualified (ProperName 'TypeName)
c1) (TypeConstructor a
_ Qualified (ProperName 'TypeName)
c2) | Qualified (ProperName 'TypeName)
c1 forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'TypeName)
c2 = (forall t. t -> Matched t
Match (), forall k a. Map k a
M.empty)
    typeHeadsAreEqual (TypeLevelString a
_ PSString
s1) (TypeLevelString a
_ PSString
s2) | PSString
s1 forall a. Eq a => a -> a -> Bool
== PSString
s2 = (forall t. t -> Matched t
Match (), forall k a. Map k a
M.empty)
    typeHeadsAreEqual (TypeLevelInt a
_ Integer
n1)    (TypeLevelInt a
_ Integer
n2)    | Integer
n1 forall a. Eq a => a -> a -> Bool
== Integer
n2 = (forall t. t -> Matched t
Match (), forall k a. Map k a
M.empty)
    typeHeadsAreEqual (TypeApp a
_ Type a
h1 Type a
t1)      (TypeApp a
_ Type a
h2 Type a
t2)                 =
      forall a.
(Matched (), Matching [Type a])
-> (Matched (), Matching [Type a])
-> (Matched (), Matching [Type a])
both (forall a. Type a -> Type a -> (Matched (), Matching [Type a])
typeHeadsAreEqual Type a
h1 Type a
h2) (forall a. Type a -> Type a -> (Matched (), Matching [Type a])
typeHeadsAreEqual Type a
t1 Type a
t2)
    typeHeadsAreEqual (KindApp a
_ Type a
h1 Type a
t1)      (KindApp a
_ Type a
h2 Type a
t2)                 =
      forall a.
(Matched (), Matching [Type a])
-> (Matched (), Matching [Type a])
-> (Matched (), Matching [Type a])
both (forall a. Type a -> Type a -> (Matched (), Matching [Type a])
typeHeadsAreEqual Type a
h1 Type a
h2) (forall a. Type a -> Type a -> (Matched (), Matching [Type a])
typeHeadsAreEqual Type a
t1 Type a
t2)
    typeHeadsAreEqual (REmpty a
_) (REmpty a
_) = (forall t. t -> Matched t
Match (), forall k a. Map k a
M.empty)
    typeHeadsAreEqual r1 :: Type a
r1@RCons{} r2 :: Type a
r2@RCons{} =
        forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a.
(Matched (), Matching [Type a])
-> (Matched (), Matching [Type a])
-> (Matched (), Matching [Type a])
both (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a.
([RowListItem a], Type a)
-> ([RowListItem a], Type a) -> (Matched (), Matching [Type a])
go (([RowListItem a], Type a), ([RowListItem a], Type a))
rest) [(Matched (), Matching [Type a])]
common
      where
        ([(Matched (), Matching [Type a])]
common, (([RowListItem a], Type a), ([RowListItem a], Type a))
rest) = forall a r.
(Label -> Type a -> Type a -> r)
-> Type a
-> Type a
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
alignRowsWith (forall a b. a -> b -> a
const forall a. Type a -> Type a -> (Matched (), Matching [Type a])
typeHeadsAreEqual) Type a
r1 Type a
r2

        go :: ([RowListItem a], Type a) -> ([RowListItem a], Type a) -> (Matched (), Matching [Type a])
        go :: forall a.
([RowListItem a], Type a)
-> ([RowListItem a], Type a) -> (Matched (), Matching [Type a])
go ([RowListItem a]
l,  KindedType a
_ Type a
t1 Type a
_) ([RowListItem a]
r,  Type a
t2)                            = forall a.
([RowListItem a], Type a)
-> ([RowListItem a], Type a) -> (Matched (), Matching [Type a])
go ([RowListItem a]
l, Type a
t1) ([RowListItem a]
r, Type a
t2)
        go ([RowListItem a]
l,  Type a
t1)                ([RowListItem a]
r,  KindedType a
_ Type a
t2 Type a
_)             = forall a.
([RowListItem a], Type a)
-> ([RowListItem a], Type a) -> (Matched (), Matching [Type a])
go ([RowListItem a]
l, Type a
t1) ([RowListItem a]
r, Type a
t2)
        go ([RowListItem a]
l,  KindApp a
_ Type a
t1 Type a
k1)   ([RowListItem a]
r,  KindApp a
_ Type a
t2 Type a
k2) | forall a b. Type a -> Type b -> Bool
eqType Type a
k1 Type a
k2 = forall a.
([RowListItem a], Type a)
-> ([RowListItem a], Type a) -> (Matched (), Matching [Type a])
go ([RowListItem a]
l, Type a
t1) ([RowListItem a]
r, Type a
t2)
        go ([], REmpty a
_)          ([], REmpty a
_)                      = (forall t. t -> Matched t
Match (), forall k a. Map k a
M.empty)
        go ([], TUnknown a
_ Int
u1)     ([], TUnknown a
_ Int
u2)      | Int
u1 forall a. Eq a => a -> a -> Bool
== Int
u2 = (forall t. t -> Matched t
Match (), forall k a. Map k a
M.empty)
        go ([], TypeVar a
_ Text
v1)      ([], TypeVar a
_ Text
v2)       | Text
v1 forall a. Eq a => a -> a -> Bool
== Text
v2 = (forall t. t -> Matched t
Match (), forall k a. Map k a
M.empty)
        go ([], Skolem a
_ Text
_ Maybe (Type a)
_ Int
sk1 SkolemScope
_)  ([], Skolem a
_ Text
_ Maybe (Type a)
_ Int
sk2 SkolemScope
_) | Int
sk1 forall a. Eq a => a -> a -> Bool
== Int
sk2 = (forall t. t -> Matched t
Match (), forall k a. Map k a
M.empty)
        go ([], TUnknown a
_ Int
_)      ([RowListItem a], Type a)
_                                   = (forall t. Matched t
Unknown, forall k a. Map k a
M.empty)
        go ([RowListItem a]
sd, Type a
r)                 ([], TypeVar a
_ Text
v)                   = (forall t. t -> Matched t
Match (), forall k a. k -> a -> Map k a
M.singleton Text
v [forall a. ([RowListItem a], Type a) -> Type a
rowFromList ([RowListItem a]
sd, Type a
r)])
        go ([RowListItem a], Type a)
_ ([RowListItem a], Type a)
_                                                         = (forall t. Matched t
Apart, forall k a. Map k a
M.empty)
    typeHeadsAreEqual (TUnknown a
_ Int
_) Type a
_ = (forall t. Matched t
Unknown, forall k a. Map k a
M.empty)
    typeHeadsAreEqual Skolem{} Type a
_       = (forall t. Matched t
Unknown, forall k a. Map k a
M.empty)
    typeHeadsAreEqual Type a
_ Type a
_ = (forall t. Matched t
Apart, forall k a. Map k a
M.empty)

    both :: (Matched (), Matching [Type a]) -> (Matched (), Matching [Type a]) -> (Matched (), Matching [Type a])
    both :: forall a.
(Matched (), Matching [Type a])
-> (Matched (), Matching [Type a])
-> (Matched (), Matching [Type a])
both (Matched ()
b1, Matching [Type a]
m1) (Matched ()
b2, Matching [Type a]
m2) = (Matched ()
b1 forall a. Semigroup a => a -> a -> a
<> Matched ()
b2, forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith forall a. [a] -> [a] -> [a]
(++) Matching [Type a]
m1 Matching [Type a]
m2)

    -- Ensure that a substitution is valid
    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

      -- Note that unknowns are only allowed to unify if they came from a type
      -- which was _not_ solved, i.e. one which was inferred by a functional
      -- dependency.
      typesAreEqual :: Type a -> Type a -> Matched ()
      typesAreEqual :: forall a. Type a -> Type a -> Matched ()
typesAreEqual (KindedType a
_ Type a
t1 Type a
_)    Type a
t2                     = forall a. Type a -> Type a -> Matched ()
typesAreEqual Type a
t1 Type a
t2
      typesAreEqual Type a
t1                     (KindedType a
_ Type a
t2 Type a
_)    = forall a. Type a -> Type a -> Matched ()
typesAreEqual Type a
t1 Type a
t2
      typesAreEqual (TUnknown a
_ Int
u1)        (TUnknown a
_ Int
u2)        | Int
u1 forall a. Eq a => a -> a -> Bool
== Int
u2 = forall t. t -> Matched t
Match ()
      typesAreEqual (TUnknown a
_ Int
u1)        Type a
t2                     = if Type a
t2 forall a. Type a -> Int -> Bool
`containsUnknown` Int
u1 then forall t. Matched t
Apart else forall t. Matched t
Unknown
      typesAreEqual Type a
t1                     (TUnknown a
_ Int
u2)        = if Type a
t1 forall a. Type a -> Int -> Bool
`containsUnknown` Int
u2 then forall t. Matched t
Apart else forall t. Matched t
Unknown
      typesAreEqual (Skolem a
_ Text
_ Maybe (Type a)
_ Int
s1 SkolemScope
_)    (Skolem a
_ Text
_ Maybe (Type a)
_ Int
s2 SkolemScope
_)    | Int
s1 forall a. Eq a => a -> a -> Bool
== Int
s2 = forall t. t -> Matched t
Match ()
      typesAreEqual (Skolem a
_ Text
_ Maybe (Type a)
_ Int
s1 SkolemScope
_)    Type a
t2                     = if Type a
t2 forall a. Type a -> Int -> Bool
`containsSkolem` Int
s1 then forall t. Matched t
Apart else forall t. Matched t
Unknown
      typesAreEqual Type a
t1                     (Skolem a
_ Text
_ Maybe (Type a)
_ Int
s2 SkolemScope
_)    = if Type a
t1 forall a. Type a -> Int -> Bool
`containsSkolem` Int
s2 then forall t. Matched t
Apart else forall t. Matched t
Unknown
      typesAreEqual (TypeVar a
_ Text
v1)         (TypeVar a
_ Text
v2)         | Text
v1 forall a. Eq a => a -> a -> Bool
== Text
v2 = forall t. t -> Matched t
Match ()
      typesAreEqual (TypeLevelString a
_ PSString
s1) (TypeLevelString a
_ PSString
s2) | PSString
s1 forall a. Eq a => a -> a -> Bool
== PSString
s2 = forall t. t -> Matched t
Match ()
      typesAreEqual (TypeLevelInt a
_ Integer
n1)    (TypeLevelInt a
_ Integer
n2)    | Integer
n1 forall a. Eq a => a -> a -> Bool
== Integer
n2 = forall t. t -> Matched t
Match ()
      typesAreEqual (TypeConstructor a
_ Qualified (ProperName 'TypeName)
c1) (TypeConstructor a
_ Qualified (ProperName 'TypeName)
c2) | Qualified (ProperName 'TypeName)
c1 forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'TypeName)
c2 = forall t. t -> Matched t
Match ()
      typesAreEqual (TypeApp a
_ Type a
h1 Type a
t1)      (TypeApp a
_ Type a
h2 Type a
t2)      = forall a. Type a -> Type a -> Matched ()
typesAreEqual Type a
h1 Type a
h2 forall a. Semigroup a => a -> a -> a
<> forall a. Type a -> Type a -> Matched ()
typesAreEqual Type a
t1 Type a
t2
      typesAreEqual (KindApp a
_ Type a
h1 Type a
t1)      (KindApp a
_ Type a
h2 Type a
t2)      = forall a. Type a -> Type a -> Matched ()
typesAreEqual Type a
h1 Type a
h2 forall a. Semigroup a => a -> a -> a
<> forall a. Type a -> Type a -> Matched ()
typesAreEqual Type a
t1 Type a
t2
      typesAreEqual (REmpty a
_)             (REmpty a
_)             = forall t. t -> Matched t
Match ()
      typesAreEqual Type a
r1                     Type a
r2                     | forall a. Type a -> Bool
isRCons Type a
r1 Bool -> Bool -> Bool
|| forall a. Type a -> Bool
isRCons Type a
r2 =
          let ([Matched ()]
common, (([RowListItem a], Type a), ([RowListItem a], Type a))
rest) = forall a r.
(Label -> Type a -> Type a -> r)
-> Type a
-> Type a
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
alignRowsWith (forall a b. a -> b -> a
const forall a. Type a -> Type a -> Matched ()
typesAreEqual) Type a
r1 Type a
r2
          in forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold [Matched ()]
common forall a. Semigroup a => a -> a -> a
<> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a.
([RowListItem a], Type a)
-> ([RowListItem a], Type a) -> Matched ()
go (([RowListItem a], Type a), ([RowListItem a], Type a))
rest
        where
          go :: ([RowListItem a], Type a) -> ([RowListItem a], Type a) -> Matched ()
          go :: forall a.
([RowListItem a], Type a)
-> ([RowListItem a], Type a) -> Matched ()
go ([RowListItem a]
l, KindedType a
_ Type a
t1 Type a
_) ([RowListItem a]
r, Type a
t2)                           = forall a.
([RowListItem a], Type a)
-> ([RowListItem a], Type a) -> Matched ()
go ([RowListItem a]
l, Type a
t1) ([RowListItem a]
r, Type a
t2)
          go ([RowListItem a]
l, Type a
t1)                ([RowListItem a]
r, KindedType a
_ Type a
t2 Type a
_)            = forall a.
([RowListItem a], Type a)
-> ([RowListItem a], Type a) -> Matched ()
go ([RowListItem a]
l, Type a
t1) ([RowListItem a]
r, Type a
t2)
          go ([], KindApp a
_ Type a
t1 Type a
k1)  ([], KindApp a
_ Type a
t2 Type a
k2)             = forall a. Type a -> Type a -> Matched ()
typesAreEqual Type a
t1 Type a
t2 forall a. Semigroup a => a -> a -> a
<> forall a. Type a -> Type a -> Matched ()
typesAreEqual Type a
k1 Type a
k2
          go ([], TUnknown a
_ Int
u1)    ([], TUnknown a
_ Int
u2)    | Int
u1 forall a. Eq a => a -> a -> Bool
== Int
u2 = forall t. t -> Matched t
Match ()
          go ([], TUnknown a
_ Int
_)     ([], Type a
_)                           = forall t. Matched t
Unknown
          go ([], Type a
_)                ([], TUnknown a
_ Int
_)                = forall t. Matched t
Unknown
          go ([], Skolem a
_ Text
_ Maybe (Type a)
_ Int
s1 SkolemScope
_)  ([], Skolem a
_ Text
_ Maybe (Type a)
_ Int
s2 SkolemScope
_)  | Int
s1 forall a. Eq a => a -> a -> Bool
== Int
s2 = forall t. t -> Matched t
Match ()
          go ([], Skolem a
_ Text
_ Maybe (Type a)
_ Int
_ SkolemScope
_)   ([RowListItem a], Type a)
_                               = forall t. Matched t
Unknown
          go ([RowListItem a], Type a)
_                      ([], Skolem a
_ Text
_ Maybe (Type a)
_ Int
_ SkolemScope
_)            = forall t. Matched t
Unknown
          go ([], REmpty a
_)         ([], REmpty a
_)                    = forall t. t -> Matched t
Match ()
          go ([], TypeVar a
_ Text
v1)     ([], TypeVar a
_ Text
v2)     | Text
v1 forall a. Eq a => a -> a -> Bool
== Text
v2 = forall t. t -> Matched t
Match ()
          go ([RowListItem a], Type a)
_  ([RowListItem a], Type a)
_                                                     = forall t. Matched t
Apart
      typesAreEqual Type a
_               Type a
_                                 = forall t. Matched t
Apart

      isRCons :: Type a -> Bool
      isRCons :: forall a. Type a -> Bool
isRCons RCons{}    = Bool
True
      isRCons Type a
_          = Bool
False

      containsSkolem :: Type a -> Int -> Bool
      containsSkolem :: forall a. Type a -> Int -> Bool
containsSkolem Type a
t Int
s = forall r a. (r -> r -> r) -> (Type a -> r) -> Type a -> r
everythingOnTypes Bool -> Bool -> Bool
(||) (\case Skolem a
_ Text
_ Maybe (Type a)
_ Int
s' SkolemScope
_ -> Int
s forall a. Eq a => a -> a -> Bool
== Int
s'; Type a
_ -> Bool
False) Type a
t

      containsUnknown :: Type a -> Int -> Bool
      containsUnknown :: forall a. Type a -> Int -> Bool
containsUnknown Type a
t Int
u = forall r a. (r -> r -> r) -> (Type a -> r) -> Type a -> r
everythingOnTypes Bool -> Bool -> Bool
(||) (\case TUnknown a
_ Int
u' -> Int
u forall a. Eq a => a -> a -> Bool
== Int
u'; Type a
_ -> Bool
False) Type a
t

-- | Add a dictionary for the constraint to the scope, and dictionaries
-- for all implied superclass instances.
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)))

-- | Check all pairs of values in a list match a predicate
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

-- | Check any pair of values in a list match a predicate
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

-- | Return all nonempty tails of a nonempty list. For example:
--
-- tails1 (fromList [1]) == fromList [fromList [1]]
-- tails1 (fromList [1,2]) == fromList [fromList [1,2], fromList [2]]
-- tails1 (fromList [1,2,3]) == fromList [fromList [1,2,3], fromList [2,3], fromList [3]]
tails1 :: NonEmpty a -> NonEmpty (NonEmpty a)
tails1 :: forall a. NonEmpty a -> NonEmpty (NonEmpty a)
tails1 =
  -- NEL.fromList is an unsafe function, but this usage should be safe, since:
  -- - `tails xs = [xs, tail xs, tail (tail xs), ..., []]`
  -- - If `xs` is nonempty, it follows that `tails xs` contains at least one nonempty
  --   list, since `head (tails xs) = xs`.
  -- - The only empty element of `tails xs` is the last one (by the definition of `tails`)
  -- - Therefore, if we take all but the last element of `tails xs` i.e.
  --   `init (tails xs)`, we have a nonempty list of nonempty lists
  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