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

import Prelude
import Protolude (ordNub)

import Control.Arrow (second, (&&&))
import Control.Monad.Error.Class (MonadError(..))
import Control.Monad.State
import Control.Monad.Supply.Class (MonadSupply(..))
import Control.Monad.Writer

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

import Language.PureScript.AST
import Language.PureScript.Crash
import Language.PureScript.Environment
import Language.PureScript.Errors
import Language.PureScript.Names
import Language.PureScript.TypeChecker.Entailment.Coercible
import Language.PureScript.TypeChecker.Entailment.IntCompare
import Language.PureScript.TypeChecker.Kinds (elaborateKind, unifyKinds')
import Language.PureScript.TypeChecker.Monad
import Language.PureScript.TypeChecker.Synonyms (replaceAllTypeSynonyms)
import Language.PureScript.TypeChecker.Unify
import Language.PureScript.TypeClassDictionaries
import Language.PureScript.Types
import Language.PureScript.Label (Label(..))
import Language.PureScript.PSString (PSString, mkString, decodeString)
import qualified Language.PureScript.Constants.Prelude as C
import qualified Language.PureScript.Constants.Prim as C

-- | 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.LT
    Ordering
EQ -> Qualified (ProperName 'ConstructorName)
C.EQ
    Ordering
GT -> Qualified (ProperName 'ConstructorName)
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)))

-- | 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

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

    valUndefined :: Expr
    valUndefined :: Expr
valUndefined = SourceSpan -> Qualified Ident -> Expr
Var SourceSpan
nullSourceSpan (forall a. QualifiedBy -> a -> Qualified a
Qualified (ModuleName -> QualifiedBy
ByModuleName ModuleName
C.Prim) (Text -> Ident
Ident forall a. IsString a => a
C.undefined))

    solve :: SourceConstraint -> WriterT (Any, [(Ident, InstanceContext, SourceConstraint)]) (StateT InstanceContext m) Expr
    solve :: SourceConstraint
-> WriterT
     (Any, [(Ident, InstanceContext, SourceConstraint)])
     (StateT InstanceContext m)
     Expr
solve = Int
-> [ErrorMessageHint]
-> SourceConstraint
-> WriterT
     (Any, [(Ident, InstanceContext, SourceConstraint)])
     (StateT InstanceContext m)
     Expr
go Int
0 [ErrorMessageHint]
hints
      where
        go :: Int -> [ErrorMessageHint] -> SourceConstraint -> WriterT (Any, [(Ident, InstanceContext, SourceConstraint)]) (StateT InstanceContext m) Expr
        go :: Int
-> [ErrorMessageHint]
-> SourceConstraint
-> WriterT
     (Any, [(Ident, InstanceContext, SourceConstraint)])
     (StateT InstanceContext m)
     Expr
go Int
work [ErrorMessageHint]
_ (Constraint (SourceSpan, [Comment])
_ Qualified (ProperName 'ClassName)
className' [SourceType]
_ [SourceType]
tys' Maybe ConstraintData
_) | Int
work forall a. Ord a => a -> a -> Bool
> Int
1000 = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpleErrorMessage -> MultipleErrors
errorMessage forall a b. (a -> b) -> a -> b
$ Qualified (ProperName 'ClassName)
-> [SourceType] -> SimpleErrorMessage
PossiblyInfiniteInstance Qualified (ProperName 'ClassName)
className' [SourceType]
tys'
        go Int
work [ErrorMessageHint]
hints' con :: SourceConstraint
con@(Constraint (SourceSpan, [Comment])
_ Qualified (ProperName 'ClassName)
className' [SourceType]
kinds' [SourceType]
tys' Maybe ConstraintData
conInfo) = forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (m :: * -> *) a.
(MonadState CheckState m, MonadError MultipleErrors m) =>
ErrorMessageHint -> m a -> m a
withErrorMessageHint (SourceConstraint -> ErrorMessageHint
ErrorSolvingConstraint SourceConstraint
con) forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT forall a b. (a -> b) -> a -> b
$ do
            -- 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.orderingLT
                  Ordering
EQ -> Qualified (ProperName 'TypeName)
C.orderingEQ
                  Ordering
GT -> Qualified (ProperName 'TypeName)
C.orderingGT
          args' :: [SourceType]
args' = [SourceType
arg0, SourceType
arg1, Qualified (ProperName 'TypeName) -> SourceType
srcTypeConstructor Qualified (ProperName 'TypeName)
ordering]
      in forall a. a -> Maybe a
Just [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 Evidence
EmptyClassInstance [] Qualified (ProperName 'ClassName)
C.SymbolCompare [] [] [SourceType]
args' forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
    solveSymbolCompare [SourceType]
_ = forall a. Maybe a
Nothing

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

    -- | 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.booleanTrue -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Reflectable
ReflectableBoolean Bool
True, SourceType
tyBoolean)
          | Qualified (ProperName 'TypeName)
n forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'TypeName)
C.booleanFalse -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Reflectable
ReflectableBoolean Bool
False, SourceType
tyBoolean)
          | Qualified (ProperName 'TypeName)
n forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'TypeName)
C.orderingLT -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ordering -> Reflectable
ReflectableOrdering Ordering
LT, Qualified (ProperName 'TypeName) -> SourceType
srcTypeConstructor Qualified (ProperName 'TypeName)
C.Ordering)
          | Qualified (ProperName 'TypeName)
n forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'TypeName)
C.orderingEQ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ordering -> Reflectable
ReflectableOrdering Ordering
EQ, Qualified (ProperName 'TypeName) -> SourceType
srcTypeConstructor Qualified (ProperName 'TypeName)
C.Ordering)
          | Qualified (ProperName 'TypeName)
n forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'TypeName)
C.orderingGT -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ordering -> Reflectable
ReflectableOrdering Ordering
GT, Qualified (ProperName 'TypeName) -> SourceType
srcTypeConstructor Qualified (ProperName 'TypeName)
C.Ordering)
        SourceType
_ -> forall a. Maybe a
Nothing
      forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall v.
Maybe ChainId
-> Integer
-> v
-> [(Qualified (ProperName 'ClassName), Integer)]
-> Qualified (ProperName 'ClassName)
-> [(Text, SourceType)]
-> [SourceType]
-> [SourceType]
-> Maybe [SourceConstraint]
-> Maybe SourceType
-> TypeClassDictionaryInScope v
TypeClassDictionaryInScope forall a. Maybe a
Nothing Integer
0 (Reflectable -> Evidence
ReflectableInstance Reflectable
ref) [] Qualified (ProperName 'ClassName)
C.Reflectable [] [] [SourceType
typeLevel, SourceType
typ] forall a. Maybe a
Nothing forall a. Maybe a
Nothing]
    solveReflectable [SourceType]
_ = forall a. Maybe a
Nothing

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

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

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

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

    -- | 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.
(Type a -> Type a -> r)
-> Type a
-> Type a
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
alignRowsWith forall a. Type a -> Type a -> (Matched (), Matching [Type a])
typeHeadsAreEqual Type a
r1 Type a
r2

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

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

    -- 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.
(Type a -> Type a -> r)
-> Type a
-> Type a
-> ([r], (([RowListItem a], Type a), ([RowListItem a], Type a)))
alignRowsWith forall a. Type a -> Type a -> Matched ()
typesAreEqual Type a
r1 Type a
r2
          in forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold [Matched ()]
common forall a. Semigroup a => a -> a -> a
<> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a.
([RowListItem a], Type a)
-> ([RowListItem a], Type a) -> Matched ()
go (([RowListItem a], Type a), ([RowListItem a], Type a))
rest
        where
          go :: ([RowListItem a], Type a) -> ([RowListItem a], Type a) -> Matched ()
          go :: forall a.
([RowListItem a], Type a)
-> ([RowListItem a], Type a) -> Matched ()
go ([RowListItem a]
l, KindedType a
_ Type a
t1 Type a
_) ([RowListItem a]
r, Type a
t2)                           = forall a.
([RowListItem a], Type a)
-> ([RowListItem a], Type a) -> Matched ()
go ([RowListItem a]
l, Type a
t1) ([RowListItem a]
r, Type a
t2)
          go ([RowListItem a]
l, Type a
t1)                ([RowListItem a]
r, KindedType a
_ Type a
t2 Type a
_)            = forall a.
([RowListItem a], Type a)
-> ([RowListItem a], Type a) -> Matched ()
go ([RowListItem a]
l, Type a
t1) ([RowListItem a]
r, Type a
t2)
          go ([], KindApp a
_ Type a
t1 Type a
k1)  ([], KindApp a
_ Type a
t2 Type a
k2)             = forall a. Type a -> Type a -> Matched ()
typesAreEqual Type a
t1 Type a
t2 forall a. Semigroup a => a -> a -> a
<> forall a. Type a -> Type a -> Matched ()
typesAreEqual Type a
k1 Type a
k2
          go ([], TUnknown a
_ Int
u1)    ([], TUnknown a
_ Int
u2)    | Int
u1 forall a. Eq a => a -> a -> Bool
== Int
u2 = forall t. t -> Matched t
Match ()
          go ([], TUnknown a
_ Int
_)     ([], Type a
_)                           = forall t. Matched t
Unknown
          go ([], Type a
_)                ([], TUnknown a
_ Int
_)                = forall t. Matched t
Unknown
          go ([], Skolem a
_ Text
_ Maybe (Type a)
_ Int
s1 SkolemScope
_)  ([], Skolem a
_ Text
_ Maybe (Type a)
_ Int
s2 SkolemScope
_)  | Int
s1 forall a. Eq a => a -> a -> Bool
== Int
s2 = forall t. t -> Matched t
Match ()
          go ([], Skolem a
_ Text
_ Maybe (Type a)
_ Int
_ SkolemScope
_)   ([RowListItem a], Type a)
_                               = forall t. Matched t
Unknown
          go ([RowListItem a], Type a)
_                      ([], Skolem a
_ Text
_ Maybe (Type a)
_ Int
_ SkolemScope
_)            = forall t. Matched t
Unknown
          go ([], REmpty a
_)         ([], REmpty a
_)                    = forall t. t -> Matched t
Match ()
          go ([], TypeVar a
_ Text
v1)     ([], TypeVar a
_ Text
v2)     | Text
v1 forall a. Eq a => a -> a -> Bool
== Text
v2 = forall t. t -> Matched t
Match ()
          go ([RowListItem a], Type a)
_  ([RowListItem a], Type a)
_                                                     = forall t. Matched t
Apart
      typesAreEqual Type a
_               Type a
_                                 = forall t. Matched t
Apart

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

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

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

-- | 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