{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ViewPatterns #-}

-- | Solve type inference constraints
--
-- In this phase we go over the constraints one by one and try to __unify__ them.
--
-- For example, if we see @Equality (TypeVar "t1") (TypeCon "Int")@, we create
-- a mapping from @t1@ to @Int@ (called a __substitution__) and
-- we go over the rest of the constraints and replace @t1@ with @Int@ (__apply the substitution__).
--
-- We also keep all the substitutions we created from the constraints (and merge them to one substitution
-- but applying new substitution to the accumulated substitution).
--
-- If we see @Equality (TypeCon "Int") (TypeCon "String")@, we throw a type error,
-- because the two types do not match.
--
-- We keep going until there are no more constraints or until we encountered an error.
--
-- The result of the algorithm is the accumulated substitution.
module Language.Giml.Types.Infer.Solve where

import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Data.List (sort)
import Data.Map qualified as M
import Data.Map.Merge.Strict qualified as M
import Data.Set qualified as S
import Language.Giml.Logging
import Language.Giml.Syntax.Ast
import Language.Giml.Types.Infer.Elaborate (ElabEnv (..), ElabState (..), genTypeVar, instantiate)
import Language.Giml.Types.Infer.Substitute
import Language.Giml.Types.Infer.Types
import Language.Giml.Utils

-- * Solve constraints

-- | Run constraint solving algorithm
solve
  :: (MonadBase b b)
  => LogAction b LogMsg
  -> Int
  -> Constraints
  -> ExceptT TypeErrorA b (Substitution, Int)
solve :: forall (b :: * -> *).
MonadBase b b =>
LogAction b LogMsg
-> Int -> Constraints -> ExceptT TypeErrorA b (Substitution, Int)
solve = LogAction b LogMsg
-> Int -> Constraints -> ExceptT TypeErrorA b (Substitution, Int)
forall (b :: * -> *).
MonadBase b b =>
LogAction b LogMsg
-> Int -> Constraints -> ExceptT TypeErrorA b (Substitution, Int)
runSolve

-- ** Types

-- | Monadic capabilities for the Solve algorithm
type Solve b m =
  ( MonadBase b m
  , MonadError TypeErrorA m
  , MonadState ElabState m -- We highjack the ElabState type for the genTypeVar function.
  , MonadReader (ElabEnv b) m
  )

-- ** Algorithm

runSolve
  :: (MonadBase b b)
  => LogAction b LogMsg
  -> Int
  -> Constraints
  -> ExceptT TypeErrorA b (Substitution, Int)
runSolve :: forall (b :: * -> *).
MonadBase b b =>
LogAction b LogMsg
-> Int -> Constraints -> ExceptT TypeErrorA b (Substitution, Int)
runSolve LogAction b LogMsg
logact Int
seed =
  ( ((Substitution, ElabState) -> (Substitution, Int))
-> ExceptT TypeErrorA b (Substitution, ElabState)
-> ExceptT TypeErrorA b (Substitution, Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ElabState -> Int)
-> (Substitution, ElabState) -> (Substitution, Int)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ElabState -> Int
esTypeVarCounter)
      (ExceptT TypeErrorA b (Substitution, ElabState)
 -> ExceptT TypeErrorA b (Substitution, Int))
-> (Constraints -> ExceptT TypeErrorA b (Substitution, ElabState))
-> Constraints
-> ExceptT TypeErrorA b (Substitution, Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StateT ElabState (ExceptT TypeErrorA b) Substitution
 -> ElabState -> ExceptT TypeErrorA b (Substitution, ElabState))
-> ElabState
-> StateT ElabState (ExceptT TypeErrorA b) Substitution
-> ExceptT TypeErrorA b (Substitution, ElabState)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT ElabState (ExceptT TypeErrorA b) Substitution
-> ElabState -> ExceptT TypeErrorA b (Substitution, ElabState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Int -> Constraints -> ElabState
ElabState Int
seed Constraints
forall a. Monoid a => a
mempty)
      (StateT ElabState (ExceptT TypeErrorA b) Substitution
 -> ExceptT TypeErrorA b (Substitution, ElabState))
-> (Constraints
    -> StateT ElabState (ExceptT TypeErrorA b) Substitution)
-> Constraints
-> ExceptT TypeErrorA b (Substitution, ElabState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ReaderT
   (ElabEnv b) (StateT ElabState (ExceptT TypeErrorA b)) Substitution
 -> ElabEnv b
 -> StateT ElabState (ExceptT TypeErrorA b) Substitution)
-> ElabEnv b
-> ReaderT
     (ElabEnv b) (StateT ElabState (ExceptT TypeErrorA b)) Substitution
-> StateT ElabState (ExceptT TypeErrorA b) Substitution
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT
  (ElabEnv b) (StateT ElabState (ExceptT TypeErrorA b)) Substitution
-> ElabEnv b
-> StateT ElabState (ExceptT TypeErrorA b) Substitution
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (Env Type
-> Env Type -> VariantEnv -> LogAction b LogMsg -> ElabEnv b
forall (b :: * -> *).
Env Type
-> Env Type -> VariantEnv -> LogAction b LogMsg -> ElabEnv b
ElabEnv Env Type
forall a. Monoid a => a
mempty Env Type
forall a. Monoid a => a
mempty VariantEnv
forall a. Monoid a => a
mempty LogAction b LogMsg
logact)
      (ReaderT
   (ElabEnv b) (StateT ElabState (ExceptT TypeErrorA b)) Substitution
 -> StateT ElabState (ExceptT TypeErrorA b) Substitution)
-> (Constraints
    -> ReaderT
         (ElabEnv b) (StateT ElabState (ExceptT TypeErrorA b)) Substitution)
-> Constraints
-> StateT ElabState (ExceptT TypeErrorA b) Substitution
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ( \[(Constraint, InputAnn)]
cs -> do
            Text
-> ReaderT (ElabEnv b) (StateT ElabState (ExceptT TypeErrorA b)) ()
forall env (b :: * -> *) (m :: * -> *).
HasLog' LogMsg env b m =>
Text -> m ()
logDetailed (Text
"Solving constraints: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [(Constraint, InputAnn)] -> Text
forall (f :: * -> *).
(Show (f Text), Functor f) =>
f (Constraint, InputAnn) -> Text
ppShowCAs [(Constraint, InputAnn)]
cs)
            Substitution
-> [(Constraint, InputAnn)]
-> ReaderT
     (ElabEnv b) (StateT ElabState (ExceptT TypeErrorA b)) Substitution
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
Substitution -> [(Constraint, InputAnn)] -> m Substitution
solveConstraints Substitution
forall a. Monoid a => a
mempty [(Constraint, InputAnn)]
cs
        )
      ([(Constraint, InputAnn)]
 -> ReaderT
      (ElabEnv b) (StateT ElabState (ExceptT TypeErrorA b)) Substitution)
-> (Constraints -> [(Constraint, InputAnn)])
-> Constraints
-> ReaderT
     (ElabEnv b) (StateT ElabState (ExceptT TypeErrorA b)) Substitution
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraints -> [(Constraint, InputAnn)]
forall a. Set a -> [a]
S.toList
  )

-- | Recursively the constraints in order, passing the accumulated substitution.
solveConstraints :: (Solve b m) => Substitution -> [ConstraintA] -> m Substitution
solveConstraints :: forall (b :: * -> *) (m :: * -> *).
Solve b m =>
Substitution -> [(Constraint, InputAnn)] -> m Substitution
solveConstraints Substitution
sub = \case
  [] -> Substitution -> m Substitution
forall (f :: * -> *) a. Applicative f => a -> f a
pure Substitution
sub
  (Constraint, InputAnn)
c : [(Constraint, InputAnn)]
cs -> do
    ([(Constraint, InputAnn)]
newCons, Substitution
newSub) <- (Constraint, InputAnn)
-> m ([(Constraint, InputAnn)], Substitution)
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
(Constraint, InputAnn)
-> m ([(Constraint, InputAnn)], Substitution)
solveConstraint (Constraint, InputAnn)
c
    -- apply the new substitution on the rest of the constraints
    [(Constraint, InputAnn)]
cs' <- Substitution
-> [(Constraint, InputAnn)] -> m [(Constraint, InputAnn)]
forall (m :: * -> *).
Substitute m =>
Substitution
-> [(Constraint, InputAnn)] -> m [(Constraint, InputAnn)]
substituteConstraints Substitution
newSub ([(Constraint, InputAnn)]
newCons [(Constraint, InputAnn)]
-> [(Constraint, InputAnn)] -> [(Constraint, InputAnn)]
forall a. Semigroup a => a -> a -> a
<> [(Constraint, InputAnn)]
cs)
    -- apply the new substitution to the accumulative substitution
    Substitution
sub' <- Substitution -> Substitution -> m Substitution
forall (m :: * -> *).
Substitute m =>
Substitution -> Substitution -> m Substitution
substituteSubs Substitution
newSub Substitution
sub
    Substitution -> [(Constraint, InputAnn)] -> m Substitution
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
Substitution -> [(Constraint, InputAnn)] -> m Substitution
solveConstraints (Substitution -> Substitution -> Substitution
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union Substitution
newSub Substitution
sub') [(Constraint, InputAnn)]
cs'

-- | Solve a constraint.
--   Returns new constraints that may arise from this constraint and a substitution
solveConstraint :: (Solve b m) => ConstraintA -> m ([ConstraintA], Substitution)
solveConstraint :: forall (b :: * -> *) (m :: * -> *).
Solve b m =>
(Constraint, InputAnn)
-> m ([(Constraint, InputAnn)], Substitution)
solveConstraint (Constraint
constraint, InputAnn
ann) = do
  Text -> m ()
forall env (b :: * -> *) (m :: * -> *).
HasLog' LogMsg env b m =>
Text -> m ()
logDetailed (Text
"constraint: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Constraint -> Text
ppShowC Constraint
constraint)
  case Constraint
constraint of
    -- For let polymorphism. Instantiate a type.
    -- See the comment on @instantiate@ for more information.
    Equality Type
t1 (TypeScheme [TypeVar]
vars Type
t2) -> do
      Type
t2' <- Text -> [TypeVar] -> Type -> m Type
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
Text -> [TypeVar] -> Type -> m Type
instantiate Text
"ti" [TypeVar]
vars Type
t2
      ([(Constraint, InputAnn)], Substitution)
-> m ([(Constraint, InputAnn)], Substitution)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Type -> Type -> Constraint
Equality Type
t1 Type
t2', InputAnn
ann)], Substitution
forall a. Monoid a => a
mempty)

    -- When the two types are equals, there's nothing to do.
    Equality Type
t1 Type
t2
      | Type
t1 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t2 ->
          ([(Constraint, InputAnn)], Substitution)
-> m ([(Constraint, InputAnn)], Substitution)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Constraint, InputAnn)]
forall a. Monoid a => a
mempty, Substitution
forall a. Monoid a => a
mempty)
    Equality (TypeApp Type
f1 Type
a1) (TypeApp Type
f2 Type
a2) ->
      ([(Constraint, InputAnn)], Substitution)
-> m ([(Constraint, InputAnn)], Substitution)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( (Constraint -> (Constraint, InputAnn))
-> [Constraint] -> [(Constraint, InputAnn)]
forall a b. (a -> b) -> [a] -> [b]
map ((Constraint -> InputAnn -> (Constraint, InputAnn))
-> InputAnn -> Constraint -> (Constraint, InputAnn)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) InputAnn
ann) ([Constraint] -> [(Constraint, InputAnn)])
-> [Constraint] -> [(Constraint, InputAnn)]
forall a b. (a -> b) -> a -> b
$ [Type -> Type -> Constraint
Equality Type
f1 Type
f2, Type -> Type -> Constraint
Equality Type
a1 Type
a2]
        , Substitution
forall a. Monoid a => a
mempty
        )
    -- all record labels and type should match
    Equality t1 :: Type
t1@(TypeRec ([(Label, Type)] -> Map Label Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Map Label Type
rec1)) t2 :: Type
t2@(TypeRec ([(Label, Type)] -> Map Label Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Map Label Type
rec2)) -> do
      let
        ([Label]
lefts, [Label]
rights, [Constraint]
matches) =
          [Matches Label Constraint] -> ([Label], [Label], [Constraint])
forall a b. [Matches a b] -> ([a], [a], [b])
unzipMatches ([Matches Label Constraint] -> ([Label], [Label], [Constraint]))
-> [Matches Label Constraint] -> ([Label], [Label], [Constraint])
forall a b. (a -> b) -> a -> b
$
            Map Label (Matches Label Constraint) -> [Matches Label Constraint]
forall k a. Map k a -> [a]
M.elems (Map Label (Matches Label Constraint)
 -> [Matches Label Constraint])
-> Map Label (Matches Label Constraint)
-> [Matches Label Constraint]
forall a b. (a -> b) -> a -> b
$
              SimpleWhenMissing Label Type (Matches Label Constraint)
-> SimpleWhenMissing Label Type (Matches Label Constraint)
-> SimpleWhenMatched Label Type Type (Matches Label Constraint)
-> Map Label Type
-> Map Label Type
-> Map Label (Matches Label Constraint)
forall k a c b.
Ord k =>
SimpleWhenMissing k a c
-> SimpleWhenMissing k b c
-> SimpleWhenMatched k a b c
-> Map k a
-> Map k b
-> Map k c
M.merge
                ((Label -> Type -> Matches Label Constraint)
-> SimpleWhenMissing Label Type (Matches Label Constraint)
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Label -> Type -> Matches Label Constraint)
 -> SimpleWhenMissing Label Type (Matches Label Constraint))
-> (Label -> Type -> Matches Label Constraint)
-> SimpleWhenMissing Label Type (Matches Label Constraint)
forall a b. (a -> b) -> a -> b
$ Matches Label Constraint -> Type -> Matches Label Constraint
forall a b. a -> b -> a
const (Matches Label Constraint -> Type -> Matches Label Constraint)
-> (Label -> Matches Label Constraint)
-> Label
-> Type
-> Matches Label Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label -> Matches Label Constraint
forall a b. a -> Matches a b
OnlyLeft)
                ((Label -> Type -> Matches Label Constraint)
-> SimpleWhenMissing Label Type (Matches Label Constraint)
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Label -> Type -> Matches Label Constraint)
 -> SimpleWhenMissing Label Type (Matches Label Constraint))
-> (Label -> Type -> Matches Label Constraint)
-> SimpleWhenMissing Label Type (Matches Label Constraint)
forall a b. (a -> b) -> a -> b
$ Matches Label Constraint -> Type -> Matches Label Constraint
forall a b. a -> b -> a
const (Matches Label Constraint -> Type -> Matches Label Constraint)
-> (Label -> Matches Label Constraint)
-> Label
-> Type
-> Matches Label Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label -> Matches Label Constraint
forall a b. a -> Matches a b
OnlyRight)
                ((Label -> Type -> Type -> Matches Label Constraint)
-> SimpleWhenMatched Label Type Type (Matches Label Constraint)
forall (f :: * -> *) k x y z.
Applicative f =>
(k -> x -> y -> z) -> WhenMatched f k x y z
M.zipWithMatched ((Label -> Type -> Type -> Matches Label Constraint)
 -> SimpleWhenMatched Label Type Type (Matches Label Constraint))
-> (Label -> Type -> Type -> Matches Label Constraint)
-> SimpleWhenMatched Label Type Type (Matches Label Constraint)
forall a b. (a -> b) -> a -> b
$ \Label
_ Type
l Type
r -> Constraint -> Matches Label Constraint
forall a b. b -> Matches a b
BothSides (Type -> Type -> Constraint
Equality Type
l Type
r))
                Map Label Type
rec1
                Map Label Type
rec2
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Label] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Label]
lefts Bool -> Bool -> Bool
&& [Label] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Label]
rights) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
        [InputAnn] -> TypeError -> m ()
forall (m :: * -> *) a.
MonadError TypeErrorA m =>
[InputAnn] -> TypeError -> m a
throwErr [InputAnn
ann] (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$
          Type -> Type -> [Label] -> [Label] -> TypeError
RecordDiff Type
t1 Type
t2 [Label]
lefts [Label]
rights
      ([(Constraint, InputAnn)], Substitution)
-> m ([(Constraint, InputAnn)], Substitution)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( (Constraint -> (Constraint, InputAnn))
-> [Constraint] -> [(Constraint, InputAnn)]
forall a b. (a -> b) -> [a] -> [b]
map ((Constraint -> InputAnn -> (Constraint, InputAnn))
-> InputAnn -> Constraint -> (Constraint, InputAnn)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) InputAnn
ann) [Constraint]
matches
        , Substitution
forall a. Monoid a => a
mempty
        )

    -- we want to make sure rec1 and rec2 do not contain matching labels with non matching types
    -- we want to match the labels from rec1 that do not exist in rec2 to match "ext"
    Equality t1 :: Type
t1@(TypeRec ([(Label, Type)] -> Map Label Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Map Label Type
rec1)) t2 :: Type
t2@(TypeRecExt ([(Label, Type)] -> Map Label Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Map Label Type
rec2) TypeVar
ext) -> do
      let
        ([(Label, Type)]
lefts, [(Label, Type)]
rights, [Constraint]
matches) =
          [Matches (Label, Type) Constraint]
-> ([(Label, Type)], [(Label, Type)], [Constraint])
forall a b. [Matches a b] -> ([a], [a], [b])
unzipMatches ([Matches (Label, Type) Constraint]
 -> ([(Label, Type)], [(Label, Type)], [Constraint]))
-> [Matches (Label, Type) Constraint]
-> ([(Label, Type)], [(Label, Type)], [Constraint])
forall a b. (a -> b) -> a -> b
$
            Map Label (Matches (Label, Type) Constraint)
-> [Matches (Label, Type) Constraint]
forall k a. Map k a -> [a]
M.elems (Map Label (Matches (Label, Type) Constraint)
 -> [Matches (Label, Type) Constraint])
-> Map Label (Matches (Label, Type) Constraint)
-> [Matches (Label, Type) Constraint]
forall a b. (a -> b) -> a -> b
$
              SimpleWhenMissing Label Type (Matches (Label, Type) Constraint)
-> SimpleWhenMissing Label Type (Matches (Label, Type) Constraint)
-> SimpleWhenMatched
     Label Type Type (Matches (Label, Type) Constraint)
-> Map Label Type
-> Map Label Type
-> Map Label (Matches (Label, Type) Constraint)
forall k a c b.
Ord k =>
SimpleWhenMissing k a c
-> SimpleWhenMissing k b c
-> SimpleWhenMatched k a b c
-> Map k a
-> Map k b
-> Map k c
M.merge
                ((Label -> Type -> Matches (Label, Type) Constraint)
-> SimpleWhenMissing Label Type (Matches (Label, Type) Constraint)
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Label -> Type -> Matches (Label, Type) Constraint)
 -> SimpleWhenMissing Label Type (Matches (Label, Type) Constraint))
-> (Label -> Type -> Matches (Label, Type) Constraint)
-> SimpleWhenMissing Label Type (Matches (Label, Type) Constraint)
forall a b. (a -> b) -> a -> b
$ ((Label, Type) -> Matches (Label, Type) Constraint)
-> (Type -> (Label, Type))
-> Type
-> Matches (Label, Type) Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Label, Type) -> Matches (Label, Type) Constraint
forall a b. a -> Matches a b
OnlyLeft ((Type -> (Label, Type))
 -> Type -> Matches (Label, Type) Constraint)
-> (Label -> Type -> (Label, Type))
-> Label
-> Type
-> Matches (Label, Type) Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,))
                ((Label -> Type -> Matches (Label, Type) Constraint)
-> SimpleWhenMissing Label Type (Matches (Label, Type) Constraint)
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Label -> Type -> Matches (Label, Type) Constraint)
 -> SimpleWhenMissing Label Type (Matches (Label, Type) Constraint))
-> (Label -> Type -> Matches (Label, Type) Constraint)
-> SimpleWhenMissing Label Type (Matches (Label, Type) Constraint)
forall a b. (a -> b) -> a -> b
$ ((Label, Type) -> Matches (Label, Type) Constraint)
-> (Type -> (Label, Type))
-> Type
-> Matches (Label, Type) Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Label, Type) -> Matches (Label, Type) Constraint
forall a b. a -> Matches a b
OnlyRight ((Type -> (Label, Type))
 -> Type -> Matches (Label, Type) Constraint)
-> (Label -> Type -> (Label, Type))
-> Label
-> Type
-> Matches (Label, Type) Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,))
                ((Label -> Type -> Type -> Matches (Label, Type) Constraint)
-> SimpleWhenMatched
     Label Type Type (Matches (Label, Type) Constraint)
forall (f :: * -> *) k x y z.
Applicative f =>
(k -> x -> y -> z) -> WhenMatched f k x y z
M.zipWithMatched ((Label -> Type -> Type -> Matches (Label, Type) Constraint)
 -> SimpleWhenMatched
      Label Type Type (Matches (Label, Type) Constraint))
-> (Label -> Type -> Type -> Matches (Label, Type) Constraint)
-> SimpleWhenMatched
     Label Type Type (Matches (Label, Type) Constraint)
forall a b. (a -> b) -> a -> b
$ \Label
_ Type
l Type
r -> Constraint -> Matches (Label, Type) Constraint
forall a b. b -> Matches a b
BothSides (Type -> Type -> Constraint
Equality Type
l Type
r))
                Map Label Type
rec1
                Map Label Type
rec2
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(Label, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Label, Type)]
rights) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
        [InputAnn] -> TypeError -> m ()
forall (m :: * -> *) a.
MonadError TypeErrorA m =>
[InputAnn] -> TypeError -> m a
throwErr [InputAnn
ann] (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$
          Type -> Type -> [Label] -> [Label] -> TypeError
RecordDiff Type
t1 Type
t2 [] (((Label, Type) -> Label) -> [(Label, Type)] -> [Label]
forall a b. (a -> b) -> [a] -> [b]
map (Label, Type) -> Label
forall a b. (a, b) -> a
fst [(Label, Type)]
rights)
      ([(Constraint, InputAnn)], Substitution)
-> m ([(Constraint, InputAnn)], Substitution)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( (Constraint -> (Constraint, InputAnn))
-> [Constraint] -> [(Constraint, InputAnn)]
forall a b. (a -> b) -> [a] -> [b]
map ((Constraint -> InputAnn -> (Constraint, InputAnn))
-> InputAnn -> Constraint -> (Constraint, InputAnn)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) InputAnn
ann) ([Constraint] -> [(Constraint, InputAnn)])
-> [Constraint] -> [(Constraint, InputAnn)]
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality ([(Label, Type)] -> Type
TypeRec [(Label, Type)]
lefts) (TypeVar -> Type
TypeVar TypeVar
ext) Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: [Constraint]
matches
        , Substitution
forall a. Monoid a => a
mempty
        )
    Equality t1 :: Type
t1@TypeRecExt {} t2 :: Type
t2@TypeRec {} -> do
      (Constraint, InputAnn)
-> m ([(Constraint, InputAnn)], Substitution)
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
(Constraint, InputAnn)
-> m ([(Constraint, InputAnn)], Substitution)
solveConstraint (Type -> Type -> Constraint
Equality Type
t2 Type
t1, InputAnn
ann)
    Equality (TypeRecExt ([(Label, Type)] -> Map Label Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Map Label Type
rec1) TypeVar
ext1) (TypeRecExt ([(Label, Type)] -> Map Label Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Map Label Type
rec2) TypeVar
ext2) -> do
      let
        matches :: [Constraint]
matches = Map Label Constraint -> [Constraint]
forall k a. Map k a -> [a]
M.elems (Map Label Constraint -> [Constraint])
-> Map Label Constraint -> [Constraint]
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> Constraint)
-> Map Label Type -> Map Label Type -> Map Label Constraint
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith Type -> Type -> Constraint
Equality Map Label Type
rec1 Map Label Type
rec2
        onlyLeft :: Map Label Type
onlyLeft = Map Label Type -> Map Label Type -> Map Label Type
forall k a b. Ord k => Map k a -> Map k b -> Map k a
M.difference Map Label Type
rec1 Map Label Type
rec2
        onlyRight :: Map Label Type
onlyRight = Map Label Type -> Map Label Type -> Map Label Type
forall k a b. Ord k => Map k a -> Map k b -> Map k a
M.difference Map Label Type
rec2 Map Label Type
rec1
      TypeVar
ext' <- Text -> m TypeVar
forall (m :: * -> *). MonadState ElabState m => Text -> m TypeVar
genTypeVar Text
"ext"
      ([(Constraint, InputAnn)], Substitution)
-> m ([(Constraint, InputAnn)], Substitution)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( (Constraint -> (Constraint, InputAnn))
-> [Constraint] -> [(Constraint, InputAnn)]
forall a b. (a -> b) -> [a] -> [b]
map ((Constraint -> InputAnn -> (Constraint, InputAnn))
-> InputAnn -> Constraint -> (Constraint, InputAnn)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) InputAnn
ann) ([Constraint] -> [(Constraint, InputAnn)])
-> [Constraint] -> [(Constraint, InputAnn)]
forall a b. (a -> b) -> a -> b
$
            Type -> Type -> Constraint
Equality ([(Label, Type)] -> TypeVar -> Type
TypeRecExt (Map Label Type -> [(Label, Type)]
forall k a. Map k a -> [(k, a)]
M.toList Map Label Type
onlyLeft) TypeVar
ext') (TypeVar -> Type
TypeVar TypeVar
ext2)
              Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: Type -> Type -> Constraint
Equality ([(Label, Type)] -> TypeVar -> Type
TypeRecExt (Map Label Type -> [(Label, Type)]
forall k a. Map k a -> [(k, a)]
M.toList Map Label Type
onlyRight) TypeVar
ext') (TypeVar -> Type
TypeVar TypeVar
ext1)
              Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: [Constraint]
matches
        , Substitution
forall a. Monoid a => a
mempty
        )

    -- Polymorphic Variants --

    -- all variants constructors and types should match
    Equality t1 :: Type
t1@(TypeVariant ([(Constr, Type)] -> Map Constr Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Map Constr Type
var1)) t2 :: Type
t2@(TypeVariant ([(Constr, Type)] -> Map Constr Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Map Constr Type
var2)) -> do
      let
        ([Constr]
lefts, [Constr]
rights, [Constraint]
matches) =
          [Matches Constr Constraint] -> ([Constr], [Constr], [Constraint])
forall a b. [Matches a b] -> ([a], [a], [b])
unzipMatches ([Matches Constr Constraint] -> ([Constr], [Constr], [Constraint]))
-> [Matches Constr Constraint]
-> ([Constr], [Constr], [Constraint])
forall a b. (a -> b) -> a -> b
$
            Map Constr (Matches Constr Constraint)
-> [Matches Constr Constraint]
forall k a. Map k a -> [a]
M.elems (Map Constr (Matches Constr Constraint)
 -> [Matches Constr Constraint])
-> Map Constr (Matches Constr Constraint)
-> [Matches Constr Constraint]
forall a b. (a -> b) -> a -> b
$
              SimpleWhenMissing Constr Type (Matches Constr Constraint)
-> SimpleWhenMissing Constr Type (Matches Constr Constraint)
-> SimpleWhenMatched Constr Type Type (Matches Constr Constraint)
-> Map Constr Type
-> Map Constr Type
-> Map Constr (Matches Constr Constraint)
forall k a c b.
Ord k =>
SimpleWhenMissing k a c
-> SimpleWhenMissing k b c
-> SimpleWhenMatched k a b c
-> Map k a
-> Map k b
-> Map k c
M.merge
                ((Constr -> Type -> Matches Constr Constraint)
-> SimpleWhenMissing Constr Type (Matches Constr Constraint)
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Constr -> Type -> Matches Constr Constraint)
 -> SimpleWhenMissing Constr Type (Matches Constr Constraint))
-> (Constr -> Type -> Matches Constr Constraint)
-> SimpleWhenMissing Constr Type (Matches Constr Constraint)
forall a b. (a -> b) -> a -> b
$ Matches Constr Constraint -> Type -> Matches Constr Constraint
forall a b. a -> b -> a
const (Matches Constr Constraint -> Type -> Matches Constr Constraint)
-> (Constr -> Matches Constr Constraint)
-> Constr
-> Type
-> Matches Constr Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constr -> Matches Constr Constraint
forall a b. a -> Matches a b
OnlyLeft)
                ((Constr -> Type -> Matches Constr Constraint)
-> SimpleWhenMissing Constr Type (Matches Constr Constraint)
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Constr -> Type -> Matches Constr Constraint)
 -> SimpleWhenMissing Constr Type (Matches Constr Constraint))
-> (Constr -> Type -> Matches Constr Constraint)
-> SimpleWhenMissing Constr Type (Matches Constr Constraint)
forall a b. (a -> b) -> a -> b
$ Matches Constr Constraint -> Type -> Matches Constr Constraint
forall a b. a -> b -> a
const (Matches Constr Constraint -> Type -> Matches Constr Constraint)
-> (Constr -> Matches Constr Constraint)
-> Constr
-> Type
-> Matches Constr Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constr -> Matches Constr Constraint
forall a b. a -> Matches a b
OnlyRight)
                ((Constr -> Type -> Type -> Matches Constr Constraint)
-> SimpleWhenMatched Constr Type Type (Matches Constr Constraint)
forall (f :: * -> *) k x y z.
Applicative f =>
(k -> x -> y -> z) -> WhenMatched f k x y z
M.zipWithMatched ((Constr -> Type -> Type -> Matches Constr Constraint)
 -> SimpleWhenMatched Constr Type Type (Matches Constr Constraint))
-> (Constr -> Type -> Type -> Matches Constr Constraint)
-> SimpleWhenMatched Constr Type Type (Matches Constr Constraint)
forall a b. (a -> b) -> a -> b
$ \Constr
_ Type
l Type
r -> Constraint -> Matches Constr Constraint
forall a b. b -> Matches a b
BothSides (Type -> Type -> Constraint
Equality Type
l Type
r))
                Map Constr Type
var1
                Map Constr Type
var2
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Constr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Constr]
lefts Bool -> Bool -> Bool
&& [Constr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Constr]
rights) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
        [InputAnn] -> TypeError -> m ()
forall (m :: * -> *) a.
MonadError TypeErrorA m =>
[InputAnn] -> TypeError -> m a
throwErr [InputAnn
ann] (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$
          Type -> Type -> [Constr] -> [Constr] -> TypeError
VariantDiff Type
t1 Type
t2 [Constr]
lefts [Constr]
rights
      ([(Constraint, InputAnn)], Substitution)
-> m ([(Constraint, InputAnn)], Substitution)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( (Constraint -> (Constraint, InputAnn))
-> [Constraint] -> [(Constraint, InputAnn)]
forall a b. (a -> b) -> [a] -> [b]
map ((Constraint -> InputAnn -> (Constraint, InputAnn))
-> InputAnn -> Constraint -> (Constraint, InputAnn)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) InputAnn
ann) [Constraint]
matches
        , Substitution
forall a. Monoid a => a
mempty
        )

    -- all relevant variants should match.
    -- When we have matching constructors from both sides, we match their type.
    Equality (TypePolyVariantLB ([(Constr, Type)] -> Map Constr Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Map Constr Type
var1) TypeVar
ext1) (TypePolyVariantLB ([(Constr, Type)] -> Map Constr Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Map Constr Type
var2) TypeVar
ext2) -> do
      let
        ([(Constr, Type)]
lefts, [(Constr, Type)]
rights, [Constraint]
matches) =
          [Matches (Constr, Type) Constraint]
-> ([(Constr, Type)], [(Constr, Type)], [Constraint])
forall a b. [Matches a b] -> ([a], [a], [b])
unzipMatches ([Matches (Constr, Type) Constraint]
 -> ([(Constr, Type)], [(Constr, Type)], [Constraint]))
-> [Matches (Constr, Type) Constraint]
-> ([(Constr, Type)], [(Constr, Type)], [Constraint])
forall a b. (a -> b) -> a -> b
$
            Map Constr (Matches (Constr, Type) Constraint)
-> [Matches (Constr, Type) Constraint]
forall k a. Map k a -> [a]
M.elems (Map Constr (Matches (Constr, Type) Constraint)
 -> [Matches (Constr, Type) Constraint])
-> Map Constr (Matches (Constr, Type) Constraint)
-> [Matches (Constr, Type) Constraint]
forall a b. (a -> b) -> a -> b
$
              SimpleWhenMissing Constr Type (Matches (Constr, Type) Constraint)
-> SimpleWhenMissing
     Constr Type (Matches (Constr, Type) Constraint)
-> SimpleWhenMatched
     Constr Type Type (Matches (Constr, Type) Constraint)
-> Map Constr Type
-> Map Constr Type
-> Map Constr (Matches (Constr, Type) Constraint)
forall k a c b.
Ord k =>
SimpleWhenMissing k a c
-> SimpleWhenMissing k b c
-> SimpleWhenMatched k a b c
-> Map k a
-> Map k b
-> Map k c
M.merge
                ((Constr -> Type -> Matches (Constr, Type) Constraint)
-> SimpleWhenMissing
     Constr Type (Matches (Constr, Type) Constraint)
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Constr -> Type -> Matches (Constr, Type) Constraint)
 -> SimpleWhenMissing
      Constr Type (Matches (Constr, Type) Constraint))
-> (Constr -> Type -> Matches (Constr, Type) Constraint)
-> SimpleWhenMissing
     Constr Type (Matches (Constr, Type) Constraint)
forall a b. (a -> b) -> a -> b
$ ((Constr, Type) -> Matches (Constr, Type) Constraint)
-> (Type -> (Constr, Type))
-> Type
-> Matches (Constr, Type) Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Constr, Type) -> Matches (Constr, Type) Constraint
forall a b. a -> Matches a b
OnlyLeft ((Type -> (Constr, Type))
 -> Type -> Matches (Constr, Type) Constraint)
-> (Constr -> Type -> (Constr, Type))
-> Constr
-> Type
-> Matches (Constr, Type) Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,))
                ((Constr -> Type -> Matches (Constr, Type) Constraint)
-> SimpleWhenMissing
     Constr Type (Matches (Constr, Type) Constraint)
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Constr -> Type -> Matches (Constr, Type) Constraint)
 -> SimpleWhenMissing
      Constr Type (Matches (Constr, Type) Constraint))
-> (Constr -> Type -> Matches (Constr, Type) Constraint)
-> SimpleWhenMissing
     Constr Type (Matches (Constr, Type) Constraint)
forall a b. (a -> b) -> a -> b
$ ((Constr, Type) -> Matches (Constr, Type) Constraint)
-> (Type -> (Constr, Type))
-> Type
-> Matches (Constr, Type) Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Constr, Type) -> Matches (Constr, Type) Constraint
forall a b. a -> Matches a b
OnlyRight ((Type -> (Constr, Type))
 -> Type -> Matches (Constr, Type) Constraint)
-> (Constr -> Type -> (Constr, Type))
-> Constr
-> Type
-> Matches (Constr, Type) Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,))
                ((Constr -> Type -> Type -> Matches (Constr, Type) Constraint)
-> SimpleWhenMatched
     Constr Type Type (Matches (Constr, Type) Constraint)
forall (f :: * -> *) k x y z.
Applicative f =>
(k -> x -> y -> z) -> WhenMatched f k x y z
M.zipWithMatched ((Constr -> Type -> Type -> Matches (Constr, Type) Constraint)
 -> SimpleWhenMatched
      Constr Type Type (Matches (Constr, Type) Constraint))
-> (Constr -> Type -> Type -> Matches (Constr, Type) Constraint)
-> SimpleWhenMatched
     Constr Type Type (Matches (Constr, Type) Constraint)
forall a b. (a -> b) -> a -> b
$ \Constr
_ Type
l Type
r -> Constraint -> Matches (Constr, Type) Constraint
forall a b. b -> Matches a b
BothSides (Type -> Type -> Constraint
Equality Type
l Type
r))
                Map Constr Type
var1
                Map Constr Type
var2
      TypeVar
ext' <- Text -> m TypeVar
forall (m :: * -> *). MonadState ElabState m => Text -> m TypeVar
genTypeVar Text
"tv"
      ([(Constraint, InputAnn)], Substitution)
-> m ([(Constraint, InputAnn)], Substitution)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( (Constraint -> (Constraint, InputAnn))
-> [Constraint] -> [(Constraint, InputAnn)]
forall a b. (a -> b) -> [a] -> [b]
map ((Constraint -> InputAnn -> (Constraint, InputAnn))
-> InputAnn -> Constraint -> (Constraint, InputAnn)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) InputAnn
ann) ([Constraint] -> [(Constraint, InputAnn)])
-> [Constraint] -> [(Constraint, InputAnn)]
forall a b. (a -> b) -> a -> b
$
            Type -> Type -> Constraint
Equality ([(Constr, Type)] -> TypeVar -> Type
TypePolyVariantLB ([(Constr, Type)] -> [(Constr, Type)]
forall a. Ord a => [a] -> [a]
sort ([(Constr, Type)] -> [(Constr, Type)])
-> [(Constr, Type)] -> [(Constr, Type)]
forall a b. (a -> b) -> a -> b
$ [(Constr, Type)]
lefts [(Constr, Type)] -> [(Constr, Type)] -> [(Constr, Type)]
forall a. Semigroup a => a -> a -> a
<> [(Constr, Type)]
rights) TypeVar
ext') (TypeVar -> Type
TypeVar TypeVar
ext1)
              Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: Type -> Type -> Constraint
Equality ([(Constr, Type)] -> TypeVar -> Type
TypePolyVariantLB ([(Constr, Type)] -> [(Constr, Type)]
forall a. Ord a => [a] -> [a]
sort ([(Constr, Type)] -> [(Constr, Type)])
-> [(Constr, Type)] -> [(Constr, Type)]
forall a b. (a -> b) -> a -> b
$ [(Constr, Type)]
lefts [(Constr, Type)] -> [(Constr, Type)] -> [(Constr, Type)]
forall a. Semigroup a => a -> a -> a
<> [(Constr, Type)]
rights) TypeVar
ext') (TypeVar -> Type
TypeVar TypeVar
ext2)
              Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: [Constraint]
matches
        , Substitution
forall a. Monoid a => a
mempty
        )

    -- to unify two upper bounded polymorphic variants with the same hidden type variant, we:
    -- 1. match the types of the known fields, and
    -- 2. merge all of the fields together into a UB that represents the merge, and
    -- 3. match it with the hidden type variable.
    -- This process keeps track of the variants we ran into for a specific type variable during constraint solving.
    Equality (TypePolyVariantUB TypeVar
tv1 ([(Constr, Type)] -> Map Constr Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Map Constr Type
var1)) (TypePolyVariantUB TypeVar
tv2 ([(Constr, Type)] -> Map Constr Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Map Constr Type
var2))
      | TypeVar
tv1 TypeVar -> TypeVar -> Bool
forall a. Eq a => a -> a -> Bool
== TypeVar
tv2 -> do
          let
            ([(Constr, Type)]
lefts, [(Constr, Type)]
rights, [((Constr, Type), Constraint)]
matches) =
              [Matches (Constr, Type) ((Constr, Type), Constraint)]
-> ([(Constr, Type)], [(Constr, Type)],
    [((Constr, Type), Constraint)])
forall a b. [Matches a b] -> ([a], [a], [b])
unzipMatches ([Matches (Constr, Type) ((Constr, Type), Constraint)]
 -> ([(Constr, Type)], [(Constr, Type)],
     [((Constr, Type), Constraint)]))
-> [Matches (Constr, Type) ((Constr, Type), Constraint)]
-> ([(Constr, Type)], [(Constr, Type)],
    [((Constr, Type), Constraint)])
forall a b. (a -> b) -> a -> b
$
                Map Constr (Matches (Constr, Type) ((Constr, Type), Constraint))
-> [Matches (Constr, Type) ((Constr, Type), Constraint)]
forall k a. Map k a -> [a]
M.elems (Map Constr (Matches (Constr, Type) ((Constr, Type), Constraint))
 -> [Matches (Constr, Type) ((Constr, Type), Constraint)])
-> Map Constr (Matches (Constr, Type) ((Constr, Type), Constraint))
-> [Matches (Constr, Type) ((Constr, Type), Constraint)]
forall a b. (a -> b) -> a -> b
$
                  SimpleWhenMissing
  Constr Type (Matches (Constr, Type) ((Constr, Type), Constraint))
-> SimpleWhenMissing
     Constr Type (Matches (Constr, Type) ((Constr, Type), Constraint))
-> SimpleWhenMatched
     Constr
     Type
     Type
     (Matches (Constr, Type) ((Constr, Type), Constraint))
-> Map Constr Type
-> Map Constr Type
-> Map Constr (Matches (Constr, Type) ((Constr, Type), Constraint))
forall k a c b.
Ord k =>
SimpleWhenMissing k a c
-> SimpleWhenMissing k b c
-> SimpleWhenMatched k a b c
-> Map k a
-> Map k b
-> Map k c
M.merge
                    ((Constr
 -> Type -> Matches (Constr, Type) ((Constr, Type), Constraint))
-> SimpleWhenMissing
     Constr Type (Matches (Constr, Type) ((Constr, Type), Constraint))
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Constr
  -> Type -> Matches (Constr, Type) ((Constr, Type), Constraint))
 -> SimpleWhenMissing
      Constr Type (Matches (Constr, Type) ((Constr, Type), Constraint)))
-> (Constr
    -> Type -> Matches (Constr, Type) ((Constr, Type), Constraint))
-> SimpleWhenMissing
     Constr Type (Matches (Constr, Type) ((Constr, Type), Constraint))
forall a b. (a -> b) -> a -> b
$ ((Constr, Type)
 -> Matches (Constr, Type) ((Constr, Type), Constraint))
-> (Type -> (Constr, Type))
-> Type
-> Matches (Constr, Type) ((Constr, Type), Constraint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Constr, Type)
-> Matches (Constr, Type) ((Constr, Type), Constraint)
forall a b. a -> Matches a b
OnlyLeft ((Type -> (Constr, Type))
 -> Type -> Matches (Constr, Type) ((Constr, Type), Constraint))
-> (Constr -> Type -> (Constr, Type))
-> Constr
-> Type
-> Matches (Constr, Type) ((Constr, Type), Constraint)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,))
                    ((Constr
 -> Type -> Matches (Constr, Type) ((Constr, Type), Constraint))
-> SimpleWhenMissing
     Constr Type (Matches (Constr, Type) ((Constr, Type), Constraint))
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Constr
  -> Type -> Matches (Constr, Type) ((Constr, Type), Constraint))
 -> SimpleWhenMissing
      Constr Type (Matches (Constr, Type) ((Constr, Type), Constraint)))
-> (Constr
    -> Type -> Matches (Constr, Type) ((Constr, Type), Constraint))
-> SimpleWhenMissing
     Constr Type (Matches (Constr, Type) ((Constr, Type), Constraint))
forall a b. (a -> b) -> a -> b
$ ((Constr, Type)
 -> Matches (Constr, Type) ((Constr, Type), Constraint))
-> (Type -> (Constr, Type))
-> Type
-> Matches (Constr, Type) ((Constr, Type), Constraint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Constr, Type)
-> Matches (Constr, Type) ((Constr, Type), Constraint)
forall a b. a -> Matches a b
OnlyRight ((Type -> (Constr, Type))
 -> Type -> Matches (Constr, Type) ((Constr, Type), Constraint))
-> (Constr -> Type -> (Constr, Type))
-> Constr
-> Type
-> Matches (Constr, Type) ((Constr, Type), Constraint)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,))
                    ((Constr
 -> Type
 -> Type
 -> Matches (Constr, Type) ((Constr, Type), Constraint))
-> SimpleWhenMatched
     Constr
     Type
     Type
     (Matches (Constr, Type) ((Constr, Type), Constraint))
forall (f :: * -> *) k x y z.
Applicative f =>
(k -> x -> y -> z) -> WhenMatched f k x y z
M.zipWithMatched ((Constr
  -> Type
  -> Type
  -> Matches (Constr, Type) ((Constr, Type), Constraint))
 -> SimpleWhenMatched
      Constr
      Type
      Type
      (Matches (Constr, Type) ((Constr, Type), Constraint)))
-> (Constr
    -> Type
    -> Type
    -> Matches (Constr, Type) ((Constr, Type), Constraint))
-> SimpleWhenMatched
     Constr
     Type
     Type
     (Matches (Constr, Type) ((Constr, Type), Constraint))
forall a b. (a -> b) -> a -> b
$ \Constr
k Type
l Type
r -> ((Constr, Type), Constraint)
-> Matches (Constr, Type) ((Constr, Type), Constraint)
forall a b. b -> Matches a b
BothSides ((Constr
k, Type
l), Type -> Type -> Constraint
Equality Type
l Type
r))
                    Map Constr Type
var1
                    Map Constr Type
var2
          ([(Constraint, InputAnn)], Substitution)
-> m ([(Constraint, InputAnn)], Substitution)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
            ( (Constraint -> (Constraint, InputAnn))
-> [Constraint] -> [(Constraint, InputAnn)]
forall a b. (a -> b) -> [a] -> [b]
map ((Constraint -> InputAnn -> (Constraint, InputAnn))
-> InputAnn -> Constraint -> (Constraint, InputAnn)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) InputAnn
ann) ([Constraint] -> [(Constraint, InputAnn)])
-> [Constraint] -> [(Constraint, InputAnn)]
forall a b. (a -> b) -> a -> b
$
                Type -> Type -> Constraint
Equality (TypeVar -> [(Constr, Type)] -> Type
TypePolyVariantUB TypeVar
tv1 ([(Constr, Type)] -> [(Constr, Type)]
forall a. Ord a => [a] -> [a]
sort ([(Constr, Type)] -> [(Constr, Type)])
-> [(Constr, Type)] -> [(Constr, Type)]
forall a b. (a -> b) -> a -> b
$ [(Constr, Type)]
lefts [(Constr, Type)] -> [(Constr, Type)] -> [(Constr, Type)]
forall a. Semigroup a => a -> a -> a
<> [(Constr, Type)]
rights [(Constr, Type)] -> [(Constr, Type)] -> [(Constr, Type)]
forall a. Semigroup a => a -> a -> a
<> (((Constr, Type), Constraint) -> (Constr, Type))
-> [((Constr, Type), Constraint)] -> [(Constr, Type)]
forall a b. (a -> b) -> [a] -> [b]
map ((Constr, Type), Constraint) -> (Constr, Type)
forall a b. (a, b) -> a
fst [((Constr, Type), Constraint)]
matches)) (TypeVar -> Type
TypeVar TypeVar
tv1)
                  Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: (((Constr, Type), Constraint) -> Constraint)
-> [((Constr, Type), Constraint)] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map ((Constr, Type), Constraint) -> Constraint
forall a b. (a, b) -> b
snd [((Constr, Type), Constraint)]
matches
            , Substitution
forall a. Monoid a => a
mempty
            )
    -- but if the type variables don't match, we treat them as regular variants that should match.
    Equality (TypePolyVariantUB TypeVar
_ [(Constr, Type)]
vars1) (TypePolyVariantUB TypeVar
_ [(Constr, Type)]
vars2) ->
      (Constraint, InputAnn)
-> m ([(Constraint, InputAnn)], Substitution)
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
(Constraint, InputAnn)
-> m ([(Constraint, InputAnn)], Substitution)
solveConstraint (Type -> Type -> Constraint
Equality ([(Constr, Type)] -> Type
TypeVariant [(Constr, Type)]
vars1) ([(Constr, Type)] -> Type
TypeVariant [(Constr, Type)]
vars2), InputAnn
ann)
    -- similar to TypeRecordExt, there shouldn't be variants in LB that we don't know of in the regular variant.
    Equality t1 :: Type
t1@(TypeVariant ([(Constr, Type)] -> Map Constr Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Map Constr Type
var1)) t2 :: Type
t2@(TypePolyVariantLB ([(Constr, Type)] -> Map Constr Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList -> Map Constr Type
var2) TypeVar
ext) -> do
      let
        ([(Constr, Type)]
lefts, [(Constr, Type)]
rights, [Constraint]
matches) =
          [Matches (Constr, Type) Constraint]
-> ([(Constr, Type)], [(Constr, Type)], [Constraint])
forall a b. [Matches a b] -> ([a], [a], [b])
unzipMatches ([Matches (Constr, Type) Constraint]
 -> ([(Constr, Type)], [(Constr, Type)], [Constraint]))
-> [Matches (Constr, Type) Constraint]
-> ([(Constr, Type)], [(Constr, Type)], [Constraint])
forall a b. (a -> b) -> a -> b
$
            Map Constr (Matches (Constr, Type) Constraint)
-> [Matches (Constr, Type) Constraint]
forall k a. Map k a -> [a]
M.elems (Map Constr (Matches (Constr, Type) Constraint)
 -> [Matches (Constr, Type) Constraint])
-> Map Constr (Matches (Constr, Type) Constraint)
-> [Matches (Constr, Type) Constraint]
forall a b. (a -> b) -> a -> b
$
              SimpleWhenMissing Constr Type (Matches (Constr, Type) Constraint)
-> SimpleWhenMissing
     Constr Type (Matches (Constr, Type) Constraint)
-> SimpleWhenMatched
     Constr Type Type (Matches (Constr, Type) Constraint)
-> Map Constr Type
-> Map Constr Type
-> Map Constr (Matches (Constr, Type) Constraint)
forall k a c b.
Ord k =>
SimpleWhenMissing k a c
-> SimpleWhenMissing k b c
-> SimpleWhenMatched k a b c
-> Map k a
-> Map k b
-> Map k c
M.merge
                ((Constr -> Type -> Matches (Constr, Type) Constraint)
-> SimpleWhenMissing
     Constr Type (Matches (Constr, Type) Constraint)
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Constr -> Type -> Matches (Constr, Type) Constraint)
 -> SimpleWhenMissing
      Constr Type (Matches (Constr, Type) Constraint))
-> (Constr -> Type -> Matches (Constr, Type) Constraint)
-> SimpleWhenMissing
     Constr Type (Matches (Constr, Type) Constraint)
forall a b. (a -> b) -> a -> b
$ ((Constr, Type) -> Matches (Constr, Type) Constraint)
-> (Type -> (Constr, Type))
-> Type
-> Matches (Constr, Type) Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Constr, Type) -> Matches (Constr, Type) Constraint
forall a b. a -> Matches a b
OnlyLeft ((Type -> (Constr, Type))
 -> Type -> Matches (Constr, Type) Constraint)
-> (Constr -> Type -> (Constr, Type))
-> Constr
-> Type
-> Matches (Constr, Type) Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,))
                ((Constr -> Type -> Matches (Constr, Type) Constraint)
-> SimpleWhenMissing
     Constr Type (Matches (Constr, Type) Constraint)
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> y) -> WhenMissing f k x y
M.mapMissing ((Constr -> Type -> Matches (Constr, Type) Constraint)
 -> SimpleWhenMissing
      Constr Type (Matches (Constr, Type) Constraint))
-> (Constr -> Type -> Matches (Constr, Type) Constraint)
-> SimpleWhenMissing
     Constr Type (Matches (Constr, Type) Constraint)
forall a b. (a -> b) -> a -> b
$ ((Constr, Type) -> Matches (Constr, Type) Constraint)
-> (Type -> (Constr, Type))
-> Type
-> Matches (Constr, Type) Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Constr, Type) -> Matches (Constr, Type) Constraint
forall a b. a -> Matches a b
OnlyRight ((Type -> (Constr, Type))
 -> Type -> Matches (Constr, Type) Constraint)
-> (Constr -> Type -> (Constr, Type))
-> Constr
-> Type
-> Matches (Constr, Type) Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,))
                ((Constr -> Type -> Type -> Matches (Constr, Type) Constraint)
-> SimpleWhenMatched
     Constr Type Type (Matches (Constr, Type) Constraint)
forall (f :: * -> *) k x y z.
Applicative f =>
(k -> x -> y -> z) -> WhenMatched f k x y z
M.zipWithMatched ((Constr -> Type -> Type -> Matches (Constr, Type) Constraint)
 -> SimpleWhenMatched
      Constr Type Type (Matches (Constr, Type) Constraint))
-> (Constr -> Type -> Type -> Matches (Constr, Type) Constraint)
-> SimpleWhenMatched
     Constr Type Type (Matches (Constr, Type) Constraint)
forall a b. (a -> b) -> a -> b
$ \Constr
_ Type
l Type
r -> Constraint -> Matches (Constr, Type) Constraint
forall a b. b -> Matches a b
BothSides (Type -> Type -> Constraint
Equality Type
l Type
r))
                Map Constr Type
var1
                Map Constr Type
var2
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(Constr, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Constr, Type)]
rights) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
        [InputAnn] -> TypeError -> m ()
forall (m :: * -> *) a.
MonadError TypeErrorA m =>
[InputAnn] -> TypeError -> m a
throwErr [InputAnn
ann] (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$
          Type -> Type -> [Constr] -> [Constr] -> TypeError
VariantDiff Type
t1 Type
t2 [] (((Constr, Type) -> Constr) -> [(Constr, Type)] -> [Constr]
forall a b. (a -> b) -> [a] -> [b]
map (Constr, Type) -> Constr
forall a b. (a, b) -> a
fst [(Constr, Type)]
rights)
      ([(Constraint, InputAnn)], Substitution)
-> m ([(Constraint, InputAnn)], Substitution)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( (Constraint -> (Constraint, InputAnn))
-> [Constraint] -> [(Constraint, InputAnn)]
forall a b. (a -> b) -> [a] -> [b]
map ((Constraint -> InputAnn -> (Constraint, InputAnn))
-> InputAnn -> Constraint -> (Constraint, InputAnn)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) InputAnn
ann) ([Constraint] -> [(Constraint, InputAnn)])
-> [Constraint] -> [(Constraint, InputAnn)]
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
Equality ([(Constr, Type)] -> Type
TypeVariant [(Constr, Type)]
lefts) (TypeVar -> Type
TypeVar TypeVar
ext) Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: [Constraint]
matches
        , Substitution
forall a. Monoid a => a
mempty
        )

    -- to unify LB and UB, we treat the UB as a normal variant.

    Equality t1 :: Type
t1@TypePolyVariantLB {} (TypePolyVariantUB TypeVar
ext [(Constr, Type)]
vars2) -> do
      ([(Constraint, InputAnn)], Substitution)
-> m ([(Constraint, InputAnn)], Substitution)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( (Type -> Type -> Constraint
Equality Type
t1 ([(Constr, Type)] -> Type
TypeVariant [(Constr, Type)]
vars2), InputAnn
ann)
            (Constraint, InputAnn)
-> [(Constraint, InputAnn)] -> [(Constraint, InputAnn)]
forall a. a -> [a] -> [a]
: (Type -> Type -> Constraint
Equality (TypeVar -> Type
TypeVar TypeVar
ext) ([(Constr, Type)] -> Type
TypeVariant []), InputAnn
ann)
            (Constraint, InputAnn)
-> [(Constraint, InputAnn)] -> [(Constraint, InputAnn)]
forall a. a -> [a] -> [a]
: []
        , Substitution
forall a. Monoid a => a
mempty
        )
    Equality (TypePolyVariantUB TypeVar
ext [(Constr, Type)]
vars1) t2 :: Type
t2@TypePolyVariantLB {} -> do
      ([(Constraint, InputAnn)], Substitution)
-> m ([(Constraint, InputAnn)], Substitution)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( (Type -> Type -> Constraint
Equality Type
t2 ([(Constr, Type)] -> Type
TypeVariant [(Constr, Type)]
vars1), InputAnn
ann)
            (Constraint, InputAnn)
-> [(Constraint, InputAnn)] -> [(Constraint, InputAnn)]
forall a. a -> [a] -> [a]
: (Type -> Type -> Constraint
Equality (TypeVar -> Type
TypeVar TypeVar
ext) ([(Constr, Type)] -> Type
TypeVariant []), InputAnn
ann)
            (Constraint, InputAnn)
-> [(Constraint, InputAnn)] -> [(Constraint, InputAnn)]
forall a. a -> [a] -> [a]
: []
        , Substitution
forall a. Monoid a => a
mempty
        )

    -- all other cases match like regular variants

    Equality t1 :: Type
t1@TypePolyVariantLB {} t2 :: Type
t2@TypeVariant {} -> do
      (Constraint, InputAnn)
-> m ([(Constraint, InputAnn)], Substitution)
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
(Constraint, InputAnn)
-> m ([(Constraint, InputAnn)], Substitution)
solveConstraint (Type -> Type -> Constraint
Equality Type
t2 Type
t1, InputAnn
ann)
    Equality (TypePolyVariantUB TypeVar
_ [(Constr, Type)]
vars) t2 :: Type
t2@TypeVariant {} -> do
      (Constraint, InputAnn)
-> m ([(Constraint, InputAnn)], Substitution)
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
(Constraint, InputAnn)
-> m ([(Constraint, InputAnn)], Substitution)
solveConstraint (Type -> Type -> Constraint
Equality ([(Constr, Type)] -> Type
TypeVariant [(Constr, Type)]
vars) Type
t2, InputAnn
ann)
    Equality t1 :: Type
t1@TypeVariant {} (TypePolyVariantUB TypeVar
_ [(Constr, Type)]
vars) -> do
      (Constraint, InputAnn)
-> m ([(Constraint, InputAnn)], Substitution)
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
(Constraint, InputAnn)
-> m ([(Constraint, InputAnn)], Substitution)
solveConstraint (Type -> Type -> Constraint
Equality Type
t1 ([(Constr, Type)] -> Type
TypeVariant [(Constr, Type)]
vars), InputAnn
ann)

    --------------------------

    -- Map a type variable to the other type
    Equality (TypeVar TypeVar
tv) Type
t2 ->
      ([(Constraint, InputAnn)], Substitution)
-> m ([(Constraint, InputAnn)], Substitution)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( [(Constraint, InputAnn)]
forall a. Monoid a => a
mempty
        , TypeVar -> (InputAnn, Type) -> Substitution
forall k a. k -> a -> Map k a
M.singleton TypeVar
tv (InputAnn
ann, Type
t2)
        )
    Equality Type
t1 (TypeVar TypeVar
tv) ->
      (Constraint, InputAnn)
-> m ([(Constraint, InputAnn)], Substitution)
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
(Constraint, InputAnn)
-> m ([(Constraint, InputAnn)], Substitution)
solveConstraint (Type -> Type -> Constraint
Equality (TypeVar -> Type
TypeVar TypeVar
tv) Type
t1, InputAnn
ann)
    -- finally, if non of the above cases matched with this empty open variant,
    -- treat it as a type variable.
    Equality (TypePolyVariantLB [] TypeVar
tv) Type
t2 ->
      (Constraint, InputAnn)
-> m ([(Constraint, InputAnn)], Substitution)
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
(Constraint, InputAnn)
-> m ([(Constraint, InputAnn)], Substitution)
solveConstraint (Type -> Type -> Constraint
Equality (TypeVar -> Type
TypeVar TypeVar
tv) Type
t2, InputAnn
ann)
    Equality Type
t1 (TypePolyVariantLB [] TypeVar
tv) ->
      (Constraint, InputAnn)
-> m ([(Constraint, InputAnn)], Substitution)
forall (b :: * -> *) (m :: * -> *).
Solve b m =>
(Constraint, InputAnn)
-> m ([(Constraint, InputAnn)], Substitution)
solveConstraint (Type -> Type -> Constraint
Equality (TypeVar -> Type
TypeVar TypeVar
tv) Type
t1, InputAnn
ann)
    -- When all else fails, throw an error.
    Equality Type
t1 Type
t2 ->
      [InputAnn]
-> TypeError -> m ([(Constraint, InputAnn)], Substitution)
forall (m :: * -> *) a.
MonadError TypeErrorA m =>
[InputAnn] -> TypeError -> m a
throwErr [InputAnn
ann] (TypeError -> m ([(Constraint, InputAnn)], Substitution))
-> TypeError -> m ([(Constraint, InputAnn)], Substitution)
forall a b. (a -> b) -> a -> b
$ Type -> Type -> TypeError
TypeMismatch Type
t1 Type
t2