-- | Handles solving kind constraints generated by
-- "Unison.KindInference.Generate".
module Unison.KindInference.Solve
  ( step,
    verify,
    initialState,
    defaultUnconstrainedVars,
    KindError (..),
    ConstraintConflict (..),
  )
where

import Control.Lens (Prism', prism', review)
import Control.Monad.Reader (asks)
import Control.Monad.Reader qualified as M
import Control.Monad.State.Strict qualified as M
import Control.Monad.Trans.Except
import Data.List.NonEmpty (NonEmpty (..))
import Data.Set qualified as Set
import Unison.Codebase.BuiltinAnnotation (BuiltinAnnotation)
import Unison.Debug (DebugFlag (KindInference), shouldDebug)
import Unison.KindInference.Constraint.Provenance (Provenance (..))
import Unison.KindInference.Constraint.Solved qualified as Solved
import Unison.KindInference.Constraint.TypeProvenance (TypeProvenance (..))
import Unison.KindInference.Constraint.Unsolved qualified as Unsolved
import Unison.KindInference.Error (ConstraintConflict (..), KindError (..), improveError)
import Unison.KindInference.Generate (builtinConstraints)
import Unison.KindInference.Generate.Monad (Gen (..), GeneratedConstraint)
import Unison.KindInference.Solve.Monad
  ( ConstraintMap,
    Descriptor (..),
    Env (..),
    Solve (..),
    SolveState (..),
    emptyState,
    run,
    runGen,
  )
import Unison.KindInference.UVar (UVar (..))
import Unison.PatternMatchCoverage.Pretty as P
import Unison.PatternMatchCoverage.UFMap qualified as U
import Unison.Prelude
import Unison.PrettyPrintEnv (PrettyPrintEnv)
import Unison.Syntax.TypePrinter qualified as TP
import Unison.Util.Pretty qualified as P
import Unison.Var (Var)

-- | Like 'GeneratedConstraint' but the provenance of @IsType@
-- constraints may be due to kind defaulting. (See 'defaultUnconstrainedVars')
type UnsolvedConstraint v loc = Unsolved.Constraint (UVar v loc) v loc TypeProvenance

-- | We feed both @UnsolvedConstraint@ and @GeneratedConstraint@ to
-- our constraint solver, so it is useful to convert
-- @GeneratedConstraint@ into @UnsolvedConstraint@ to avoid code
-- duplication.
_Generated :: forall v loc. Prism' (UnsolvedConstraint v loc) (GeneratedConstraint v loc)
_Generated :: forall v loc (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (GeneratedConstraint v loc) (f (GeneratedConstraint v loc))
-> p (UnsolvedConstraint v loc) (f (UnsolvedConstraint v loc))
_Generated = (GeneratedConstraint v loc -> UnsolvedConstraint v loc)
-> (UnsolvedConstraint v loc -> Maybe (GeneratedConstraint v loc))
-> Prism
     (UnsolvedConstraint v loc)
     (UnsolvedConstraint v loc)
     (GeneratedConstraint v loc)
     (GeneratedConstraint v loc)
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism' ((Provenance v loc -> Identity (TypeProvenance v loc))
-> GeneratedConstraint v loc -> Identity (UnsolvedConstraint v loc)
forall uv v loc (prov :: * -> * -> *) (prov' :: * -> * -> *)
       (f :: * -> *).
Applicative f =>
(prov v loc -> f (prov' v loc))
-> Constraint uv v loc prov -> f (Constraint uv v loc prov')
Unsolved.typeProv ((Provenance v loc -> Identity (TypeProvenance v loc))
 -> GeneratedConstraint v loc
 -> Identity (UnsolvedConstraint v loc))
-> (Provenance v loc -> TypeProvenance v loc)
-> GeneratedConstraint v loc
-> UnsolvedConstraint v loc
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Provenance v loc -> TypeProvenance v loc
forall v loc. Provenance v loc -> TypeProvenance v loc
NotDefault) \case
  Unsolved.IsType UVar v loc
s TypeProvenance v loc
l -> case TypeProvenance v loc
l of
    TypeProvenance v loc
Default -> Maybe (GeneratedConstraint v loc)
forall a. Maybe a
Nothing
    NotDefault Provenance v loc
l -> GeneratedConstraint v loc -> Maybe (GeneratedConstraint v loc)
forall a. a -> Maybe a
Just (UVar v loc -> Provenance v loc -> GeneratedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
uv -> typeProv v loc -> Constraint uv v loc typeProv
Unsolved.IsType UVar v loc
s Provenance v loc
l)
  Unsolved.IsAbility UVar v loc
s Provenance v loc
l -> GeneratedConstraint v loc -> Maybe (GeneratedConstraint v loc)
forall a. a -> Maybe a
Just (UVar v loc -> Provenance v loc -> GeneratedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
uv -> Provenance v loc -> Constraint uv v loc typeProv
Unsolved.IsAbility UVar v loc
s Provenance v loc
l)
  Unsolved.IsArr UVar v loc
s Provenance v loc
l UVar v loc
a UVar v loc
b -> GeneratedConstraint v loc -> Maybe (GeneratedConstraint v loc)
forall a. a -> Maybe a
Just (UVar v loc
-> Provenance v loc
-> UVar v loc
-> UVar v loc
-> GeneratedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
uv -> Provenance v loc -> uv -> uv -> Constraint uv v loc typeProv
Unsolved.IsArr UVar v loc
s Provenance v loc
l UVar v loc
a UVar v loc
b)
  Unsolved.Unify Provenance v loc
l UVar v loc
a UVar v loc
b -> GeneratedConstraint v loc -> Maybe (GeneratedConstraint v loc)
forall a. a -> Maybe a
Just (Provenance v loc
-> UVar v loc -> UVar v loc -> GeneratedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
Provenance v loc -> uv -> uv -> Constraint uv v loc typeProv
Unsolved.Unify Provenance v loc
l UVar v loc
a UVar v loc
b)

-- | This is the primary function in the exposed API. @step@ applies
-- some generated constraints to a solve state, returning a kind error
-- if detected or a new solve state.
step ::
  (Var v, Ord loc, Show loc) =>
  Env ->
  SolveState v loc ->
  [GeneratedConstraint v loc] ->
  Either (NonEmpty (KindError v loc)) (SolveState v loc)
step :: forall v loc.
(Var v, Ord loc, Show loc) =>
Env
-> SolveState v loc
-> [GeneratedConstraint v loc]
-> Either (NonEmpty (KindError v loc)) (SolveState v loc)
step Env
e SolveState v loc
st [GeneratedConstraint v loc]
cs =
  let action :: Solve v loc (Either (NonEmpty (KindError v loc)) ())
action = do
        [GeneratedConstraint v loc] -> Solve v loc [KindError v loc]
forall v loc.
(Show loc, Var v, Ord loc) =>
[GeneratedConstraint v loc] -> Solve v loc [KindError v loc]
reduce [GeneratedConstraint v loc]
cs Solve v loc [KindError v loc]
-> ([KindError v loc]
    -> Solve v loc (Either (NonEmpty (KindError v loc)) ()))
-> Solve v loc (Either (NonEmpty (KindError v loc)) ())
forall a b. Solve v loc a -> (a -> Solve v loc b) -> Solve v loc b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          [] -> Either (NonEmpty (KindError v loc)) ()
-> Solve v loc (Either (NonEmpty (KindError v loc)) ())
forall a. a -> Solve v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (() -> Either (NonEmpty (KindError v loc)) ()
forall a b. b -> Either a b
Right ())
          KindError v loc
e : [KindError v loc]
es -> do
            -- We have an error, but do an occ check first to ensure
            -- we present the most sensible error.
            SolveState v loc
st <- Solve v loc (SolveState v loc)
forall s (m :: * -> *). MonadState s m => m s
M.get
            case SolveState v loc
-> Either (NonEmpty (KindError v loc)) (SolveState v loc)
forall v loc.
Var v =>
SolveState v loc
-> Either (NonEmpty (KindError v loc)) (SolveState v loc)
verify SolveState v loc
st of
              Left NonEmpty (KindError v loc)
e -> Either (NonEmpty (KindError v loc)) ()
-> Solve v loc (Either (NonEmpty (KindError v loc)) ())
forall a. a -> Solve v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NonEmpty (KindError v loc)
-> Either (NonEmpty (KindError v loc)) ()
forall a b. a -> Either a b
Left NonEmpty (KindError v loc)
e)
              Right SolveState v loc
_ -> do
                NonEmpty (KindError v loc)
-> Either (NonEmpty (KindError v loc)) ()
forall a b. a -> Either a b
Left (NonEmpty (KindError v loc)
 -> Either (NonEmpty (KindError v loc)) ())
-> Solve v loc (NonEmpty (KindError v loc))
-> Solve v loc (Either (NonEmpty (KindError v loc)) ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (KindError v loc -> Solve v loc (KindError v loc))
-> NonEmpty (KindError v loc)
-> Solve v loc (NonEmpty (KindError v loc))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NonEmpty a -> f (NonEmpty b)
traverse KindError v loc -> Solve v loc (KindError v loc)
forall v loc.
Var v =>
KindError v loc -> Solve v loc (KindError v loc)
improveError (KindError v loc
e KindError v loc -> [KindError v loc] -> NonEmpty (KindError v loc)
forall a. a -> [a] -> NonEmpty a
:| [KindError v loc]
es)
   in case Solve v loc (Either (NonEmpty (KindError v loc)) ())
-> Env
-> SolveState v loc
-> (Either (NonEmpty (KindError v loc)) (), SolveState v loc)
forall v loc a.
Solve v loc a -> Env -> SolveState v loc -> (a, SolveState v loc)
unSolve Solve v loc (Either (NonEmpty (KindError v loc)) ())
action Env
e SolveState v loc
st of
        (Either (NonEmpty (KindError v loc)) ()
res, SolveState v loc
finalState) -> case Either (NonEmpty (KindError v loc)) ()
res of
          Left NonEmpty (KindError v loc)
e -> NonEmpty (KindError v loc)
-> Either (NonEmpty (KindError v loc)) (SolveState v loc)
forall a b. a -> Either a b
Left NonEmpty (KindError v loc)
e
          Right () -> SolveState v loc
-> Either (NonEmpty (KindError v loc)) (SolveState v loc)
forall a b. b -> Either a b
Right SolveState v loc
finalState

-- | Default any unconstrained vars to @Type@
defaultUnconstrainedVars :: (Var v) => SolveState v loc -> SolveState v loc
defaultUnconstrainedVars :: forall v loc. Var v => SolveState v loc -> SolveState v loc
defaultUnconstrainedVars SolveState v loc
st =
  let newConstraints :: UFMap (UVar v loc) (Descriptor v loc)
newConstraints = (UFMap (UVar v loc) (Descriptor v loc)
 -> UVar v loc -> UFMap (UVar v loc) (Descriptor v loc))
-> UFMap (UVar v loc) (Descriptor v loc)
-> [UVar v loc]
-> UFMap (UVar v loc) (Descriptor v loc)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' UFMap (UVar v loc) (Descriptor v loc)
-> UVar v loc -> UFMap (UVar v loc) (Descriptor v loc)
forall {k} {v} {loc}.
Ord k =>
UFMap k (Descriptor v loc) -> k -> UFMap k (Descriptor v loc)
phi (SolveState v loc -> UFMap (UVar v loc) (Descriptor v loc)
forall v loc.
SolveState v loc -> UFMap (UVar v loc) (Descriptor v loc)
constraints SolveState v loc
st) (SolveState v loc -> [UVar v loc]
forall v loc. SolveState v loc -> [UVar v loc]
newUnifVars SolveState v loc
st)
      phi :: UFMap k (Descriptor v loc) -> k -> UFMap k (Descriptor v loc)
phi UFMap k (Descriptor v loc)
b k
a = k
-> Maybe (Descriptor v loc)
-> (k -> Int -> Descriptor v loc -> UFValue k (Descriptor v loc))
-> UFMap k (Descriptor v loc)
-> UFMap k (Descriptor v loc)
forall k v.
Ord k =>
k
-> Maybe v
-> (k -> Int -> v -> UFValue k v)
-> UFMap k v
-> UFMap k v
U.alter k
a Maybe (Descriptor v loc)
forall {a}. a
handleNothing k -> Int -> Descriptor v loc -> UFValue k (Descriptor v loc)
forall {p} {v} {loc} {k}.
p -> Int -> Descriptor v loc -> UFValue k (Descriptor v loc)
handleJust UFMap k (Descriptor v loc)
b
      handleNothing :: a
handleNothing = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible"
      handleJust :: p -> Int -> Descriptor v loc -> UFValue k (Descriptor v loc)
handleJust p
_canonK Int
ecSize Descriptor v loc
d = case Descriptor v loc -> Maybe (Constraint (UVar v loc) v loc)
forall v loc.
Descriptor v loc -> Maybe (Constraint (UVar v loc) v loc)
descriptorConstraint Descriptor v loc
d of
        Maybe (Constraint (UVar v loc) v loc)
Nothing -> Int -> Descriptor v loc -> UFValue k (Descriptor v loc)
forall k v. Int -> v -> UFValue k v
U.Canonical Int
ecSize Descriptor v loc
d {descriptorConstraint = Just $ Solved.IsType Default}
        Just Constraint (UVar v loc) v loc
_ -> Int -> Descriptor v loc -> UFValue k (Descriptor v loc)
forall k v. Int -> v -> UFValue k v
U.Canonical Int
ecSize Descriptor v loc
d
   in SolveState v loc
st {constraints = newConstraints, newUnifVars = []}

-- | Loop through the constraints, eliminating constraints until we
-- have some set that cannot be reduced. There isn't any strong reason
-- to avoid halting at the first error -- we don't have constraints
-- that error but may succeed with more information or anything. The
-- idea of looping was to resolve as much as possible so that the
-- error message can be as filled out as possible.
reduce ::
  forall v loc.
  (Show loc, Var v, Ord loc) =>
  [GeneratedConstraint v loc] ->
  Solve v loc [KindError v loc]
reduce :: forall v loc.
(Show loc, Var v, Ord loc) =>
[GeneratedConstraint v loc] -> Solve v loc [KindError v loc]
reduce [GeneratedConstraint v loc]
cs0 = Pretty ColorText
-> [GeneratedConstraint v loc]
-> ([GeneratedConstraint v loc] -> Solve v loc [KindError v loc])
-> Solve v loc [KindError v loc]
forall a.
Pretty ColorText
-> [GeneratedConstraint v loc]
-> ([GeneratedConstraint v loc] -> Solve v loc a)
-> Solve v loc a
dbg Pretty ColorText
"reduce" [GeneratedConstraint v loc]
cs0 (Bool
-> [GeneratedConstraint v loc]
-> [GeneratedConstraint v loc]
-> Solve v loc [KindError v loc]
go Bool
False [])
  where
    go :: Bool
-> [GeneratedConstraint v loc]
-> [GeneratedConstraint v loc]
-> Solve v loc [KindError v loc]
go Bool
b [GeneratedConstraint v loc]
acc = \case
      [] -> case Bool
b of
        Bool
True -> Pretty ColorText
-> [GeneratedConstraint v loc]
-> ([GeneratedConstraint v loc] -> Solve v loc [KindError v loc])
-> Solve v loc [KindError v loc]
forall a.
Pretty ColorText
-> [GeneratedConstraint v loc]
-> ([GeneratedConstraint v loc] -> Solve v loc a)
-> Solve v loc a
dbg Pretty ColorText
"go" [GeneratedConstraint v loc]
acc (Bool
-> [GeneratedConstraint v loc]
-> [GeneratedConstraint v loc]
-> Solve v loc [KindError v loc]
go Bool
False [])
        Bool
False -> [GeneratedConstraint v loc]
-> (GeneratedConstraint v loc -> Solve v loc (KindError v loc))
-> Solve v loc [KindError v loc]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [GeneratedConstraint v loc]
acc \GeneratedConstraint v loc
c ->
          Pretty ColorText
-> GeneratedConstraint v loc
-> (GeneratedConstraint v loc
    -> Solve v loc (Either (KindError v loc) ()))
-> Solve v loc (Either (KindError v loc) ())
forall a.
Pretty ColorText
-> GeneratedConstraint v loc
-> (GeneratedConstraint v loc -> Solve v loc a)
-> Solve v loc a
dbgSingle Pretty ColorText
"failed to add constraint" GeneratedConstraint v loc
c GeneratedConstraint v loc
-> Solve v loc (Either (KindError v loc) ())
forall v loc.
(Ord loc, Var v) =>
GeneratedConstraint v loc
-> Solve v loc (Either (KindError v loc) ())
addConstraint Solve v loc (Either (KindError v loc) ())
-> (Either (KindError v loc) () -> Solve v loc (KindError v loc))
-> Solve v loc (KindError v loc)
forall a b. Solve v loc a -> (a -> Solve v loc b) -> Solve v loc b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Left KindError v loc
x -> KindError v loc -> Solve v loc (KindError v loc)
forall a. a -> Solve v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure KindError v loc
x
            Right () -> [Char] -> Solve v loc (KindError v loc)
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible"
      GeneratedConstraint v loc
c : [GeneratedConstraint v loc]
cs ->
        GeneratedConstraint v loc
-> Solve v loc (Either (KindError v loc) ())
forall v loc.
(Ord loc, Var v) =>
GeneratedConstraint v loc
-> Solve v loc (Either (KindError v loc) ())
addConstraint GeneratedConstraint v loc
c Solve v loc (Either (KindError v loc) ())
-> (Either (KindError v loc) () -> Solve v loc [KindError v loc])
-> Solve v loc [KindError v loc]
forall a b. Solve v loc a -> (a -> Solve v loc b) -> Solve v loc b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          -- If an error occurs then push it back onto the unsolved
          -- stack
          Left KindError v loc
_ -> Bool
-> [GeneratedConstraint v loc]
-> [GeneratedConstraint v loc]
-> Solve v loc [KindError v loc]
go Bool
b (GeneratedConstraint v loc
c GeneratedConstraint v loc
-> [GeneratedConstraint v loc] -> [GeneratedConstraint v loc]
forall a. a -> [a] -> [a]
: [GeneratedConstraint v loc]
acc) [GeneratedConstraint v loc]
cs
          -- Signal that we solved something on this pass (by passing
          -- @True@) and continue
          Right () -> Bool
-> [GeneratedConstraint v loc]
-> [GeneratedConstraint v loc]
-> Solve v loc [KindError v loc]
go Bool
True [GeneratedConstraint v loc]
acc [GeneratedConstraint v loc]
cs

    -- \| tracing helper
    dbg ::
      forall a.
      -- \| A hanging prefix or header
      P.Pretty P.ColorText ->
      -- \| The constraints to print
      [GeneratedConstraint v loc] ->
      ([GeneratedConstraint v loc] -> Solve v loc a) ->
      Solve v loc a
    dbg :: forall a.
Pretty ColorText
-> [GeneratedConstraint v loc]
-> ([GeneratedConstraint v loc] -> Solve v loc a)
-> Solve v loc a
dbg = (PrettyPrintEnv -> [GeneratedConstraint v loc] -> Pretty ColorText)
-> Pretty ColorText
-> [GeneratedConstraint v loc]
-> ([GeneratedConstraint v loc] -> Solve v loc a)
-> Solve v loc a
forall a b.
(PrettyPrintEnv -> a -> Pretty ColorText)
-> Pretty ColorText -> a -> (a -> Solve v loc b) -> Solve v loc b
traceApp \PrettyPrintEnv
ppe [GeneratedConstraint v loc]
cs -> PrettyPrintEnv -> [UnsolvedConstraint v loc] -> Pretty ColorText
forall loc v.
(Show loc, Var v) =>
PrettyPrintEnv -> [UnsolvedConstraint v loc] -> Pretty ColorText
prettyConstraints PrettyPrintEnv
ppe ((GeneratedConstraint v loc -> UnsolvedConstraint v loc)
-> [GeneratedConstraint v loc] -> [UnsolvedConstraint v loc]
forall a b. (a -> b) -> [a] -> [b]
map (AReview (UnsolvedConstraint v loc) (GeneratedConstraint v loc)
-> GeneratedConstraint v loc -> UnsolvedConstraint v loc
forall b (m :: * -> *) t. MonadReader b m => AReview t b -> m t
review AReview (UnsolvedConstraint v loc) (GeneratedConstraint v loc)
forall v loc (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (GeneratedConstraint v loc) (f (GeneratedConstraint v loc))
-> p (UnsolvedConstraint v loc) (f (UnsolvedConstraint v loc))
_Generated) [GeneratedConstraint v loc]
cs)

    -- \| Like @dbg@, but for a single constraint
    dbgSingle ::
      forall a.
      P.Pretty P.ColorText ->
      GeneratedConstraint v loc ->
      (GeneratedConstraint v loc -> Solve v loc a) ->
      Solve v loc a
    dbgSingle :: forall a.
Pretty ColorText
-> GeneratedConstraint v loc
-> (GeneratedConstraint v loc -> Solve v loc a)
-> Solve v loc a
dbgSingle = (PrettyPrintEnv -> GeneratedConstraint v loc -> Pretty ColorText)
-> Pretty ColorText
-> GeneratedConstraint v loc
-> (GeneratedConstraint v loc -> Solve v loc a)
-> Solve v loc a
forall a b.
(PrettyPrintEnv -> a -> Pretty ColorText)
-> Pretty ColorText -> a -> (a -> Solve v loc b) -> Solve v loc b
traceApp \PrettyPrintEnv
ppe GeneratedConstraint v loc
c -> PrettyPrintEnv -> UnsolvedConstraint v loc -> Pretty ColorText
forall loc v.
(Show loc, Var v) =>
PrettyPrintEnv -> UnsolvedConstraint v loc -> Pretty ColorText
prettyConstraintD' PrettyPrintEnv
ppe (AReview (UnsolvedConstraint v loc) (GeneratedConstraint v loc)
-> GeneratedConstraint v loc -> UnsolvedConstraint v loc
forall b (m :: * -> *) t. MonadReader b m => AReview t b -> m t
review AReview (UnsolvedConstraint v loc) (GeneratedConstraint v loc)
forall v loc (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (GeneratedConstraint v loc) (f (GeneratedConstraint v loc))
-> p (UnsolvedConstraint v loc) (f (UnsolvedConstraint v loc))
_Generated GeneratedConstraint v loc
c)

    -- \| A helper for @dbg*@
    traceApp ::
      forall a b.
      (PrettyPrintEnv -> a -> P.Pretty P.ColorText) ->
      P.Pretty P.ColorText ->
      a ->
      (a -> Solve v loc b) ->
      Solve v loc b
    traceApp :: forall a b.
(PrettyPrintEnv -> a -> Pretty ColorText)
-> Pretty ColorText -> a -> (a -> Solve v loc b) -> Solve v loc b
traceApp PrettyPrintEnv -> a -> Pretty ColorText
prettyA Pretty ColorText
hdr a
a a -> Solve v loc b
ab =
      case DebugFlag -> Bool
shouldDebug DebugFlag
KindInference of
        Bool
False -> a -> Solve v loc b
ab a
a
        Bool
True -> do
          PrettyPrintEnv
ppe <- (Env -> PrettyPrintEnv) -> Solve v loc PrettyPrintEnv
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Env -> PrettyPrintEnv
prettyPrintEnv
          Pretty ColorText -> Solve v loc b -> Solve v loc b
forall a. Pretty ColorText -> a -> a
tracePretty (Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall s.
(ListLike s Char, IsString s) =>
Pretty s -> Pretty s -> Pretty s
P.hang (Pretty ColorText -> Pretty ColorText
P.bold Pretty ColorText
hdr) (PrettyPrintEnv -> a -> Pretty ColorText
prettyA PrettyPrintEnv
ppe a
a)) (a -> Solve v loc b
ab a
a)

-- | Add a single constraint, returning an error if there is a
-- contradictory constraint.
addConstraint ::
  forall v loc.
  (Ord loc, Var v) =>
  GeneratedConstraint v loc ->
  Solve v loc (Either (KindError v loc) ())
addConstraint :: forall v loc.
(Ord loc, Var v) =>
GeneratedConstraint v loc
-> Solve v loc (Either (KindError v loc) ())
addConstraint GeneratedConstraint v loc
constraint = do
  SolveState v loc
initialState <- Solve v loc (SolveState v loc)
forall s (m :: * -> *). MonadState s m => m s
M.get

  -- Process implied constraints until they are all solved or an error
  -- is encountered
  let processPostAction ::
        Either (ConstraintConflict v loc) [UnsolvedConstraint v loc] ->
        Solve v loc (Either (KindError v loc) ())
      processPostAction :: Either (ConstraintConflict v loc) [UnsolvedConstraint v loc]
-> Solve v loc (Either (KindError v loc) ())
processPostAction = \case
        -- failure
        Left ConstraintConflict v loc
cc -> do
          -- roll back state changes
          SolveState v loc -> Solve v loc ()
forall s (m :: * -> *). MonadState s m => s -> m ()
M.put SolveState v loc
initialState
          pure (KindError v loc -> Either (KindError v loc) ()
forall a b. a -> Either a b
Left (GeneratedConstraint v loc
-> ConstraintConflict v loc
-> ConstraintMap v loc
-> KindError v loc
forall v loc.
GeneratedConstraint v loc
-> ConstraintConflict v loc
-> ConstraintMap v loc
-> KindError v loc
ConstraintConflict GeneratedConstraint v loc
constraint ConstraintConflict v loc
cc (SolveState v loc -> ConstraintMap v loc
forall v loc.
SolveState v loc -> UFMap (UVar v loc) (Descriptor v loc)
constraints SolveState v loc
initialState)))
        -- success
        Right [] -> Either (KindError v loc) ()
-> Solve v loc (Either (KindError v loc) ())
forall a. a -> Solve v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (() -> Either (KindError v loc) ()
forall a b. b -> Either a b
Right ())
        -- undetermined
        Right (UnsolvedConstraint v loc
x : [UnsolvedConstraint v loc]
xs) -> do
          -- we could return a list of kind errors that are implied by
          -- this constraint, but for now we just return the first
          -- contradiction.
          Either (ConstraintConflict v loc) [UnsolvedConstraint v loc]
-> Solve v loc (Either (KindError v loc) ())
processPostAction (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc]
 -> Solve v loc (Either (KindError v loc) ()))
-> (Either (ConstraintConflict v loc) [[UnsolvedConstraint v loc]]
    -> Either (ConstraintConflict v loc) [UnsolvedConstraint v loc])
-> Either (ConstraintConflict v loc) [[UnsolvedConstraint v loc]]
-> Solve v loc (Either (KindError v loc) ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([[UnsolvedConstraint v loc]] -> [UnsolvedConstraint v loc])
-> Either (ConstraintConflict v loc) [[UnsolvedConstraint v loc]]
-> Either (ConstraintConflict v loc) [UnsolvedConstraint v loc]
forall a b.
(a -> b)
-> Either (ConstraintConflict v loc) a
-> Either (ConstraintConflict v loc) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[UnsolvedConstraint v loc]] -> [UnsolvedConstraint v loc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Either (ConstraintConflict v loc) [[UnsolvedConstraint v loc]]
 -> Solve v loc (Either (KindError v loc) ()))
-> Solve
     v
     loc
     (Either (ConstraintConflict v loc) [[UnsolvedConstraint v loc]])
-> Solve v loc (Either (KindError v loc) ())
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExceptT
  (ConstraintConflict v loc)
  (Solve v loc)
  [[UnsolvedConstraint v loc]]
-> Solve
     v
     loc
     (Either (ConstraintConflict v loc) [[UnsolvedConstraint v loc]])
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (((UnsolvedConstraint v loc
 -> ExceptT
      (ConstraintConflict v loc)
      (Solve v loc)
      [UnsolvedConstraint v loc])
-> [UnsolvedConstraint v loc]
-> ExceptT
     (ConstraintConflict v loc)
     (Solve v loc)
     [[UnsolvedConstraint v loc]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Solve
  v
  loc
  (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc])
-> ExceptT
     (ConstraintConflict v loc) (Solve v loc) [UnsolvedConstraint v loc]
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (Solve
   v
   loc
   (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc])
 -> ExceptT
      (ConstraintConflict v loc)
      (Solve v loc)
      [UnsolvedConstraint v loc])
-> (UnsolvedConstraint v loc
    -> Solve
         v
         loc
         (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc]))
-> UnsolvedConstraint v loc
-> ExceptT
     (ConstraintConflict v loc) (Solve v loc) [UnsolvedConstraint v loc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnsolvedConstraint v loc
-> Solve
     v
     loc
     (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc])
forall v loc.
(Ord loc, Var v) =>
UnsolvedConstraint v loc
-> Solve
     v
     loc
     (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc])
addConstraint') (UnsolvedConstraint v loc
x UnsolvedConstraint v loc
-> [UnsolvedConstraint v loc] -> [UnsolvedConstraint v loc]
forall a. a -> [a] -> [a]
: [UnsolvedConstraint v loc]
xs)))
  Either (ConstraintConflict v loc) [UnsolvedConstraint v loc]
-> Solve v loc (Either (KindError v loc) ())
processPostAction (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc]
 -> Solve v loc (Either (KindError v loc) ()))
-> Solve
     v
     loc
     (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc])
-> Solve v loc (Either (KindError v loc) ())
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< UnsolvedConstraint v loc
-> Solve
     v
     loc
     (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc])
forall v loc.
(Ord loc, Var v) =>
UnsolvedConstraint v loc
-> Solve
     v
     loc
     (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc])
addConstraint' (AReview (UnsolvedConstraint v loc) (GeneratedConstraint v loc)
-> GeneratedConstraint v loc -> UnsolvedConstraint v loc
forall b (m :: * -> *) t. MonadReader b m => AReview t b -> m t
review AReview (UnsolvedConstraint v loc) (GeneratedConstraint v loc)
forall v loc (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (GeneratedConstraint v loc) (f (GeneratedConstraint v loc))
-> p (UnsolvedConstraint v loc) (f (UnsolvedConstraint v loc))
_Generated GeneratedConstraint v loc
constraint)

-- | Decompose the unsolved constraint into implied constraints,
-- returning a constraint conflict if the constraint cannot be
-- satisfied.
addConstraint' ::
  forall v loc.
  (Ord loc, Var v) =>
  UnsolvedConstraint v loc ->
  Solve v loc (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc])
addConstraint' :: forall v loc.
(Ord loc, Var v) =>
UnsolvedConstraint v loc
-> Solve
     v
     loc
     (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc])
addConstraint' = \case
  -- @IsAbility@ and @IsType@ constraints are very straightforward,
  -- they are satisfied of the constraint already exists or no
  -- constraint exists.
  Unsolved.IsAbility UVar v loc
s Provenance v loc
p0 -> do
    UVar v loc
-> Constraint (UVar v loc) v loc
-> (Constraint (UVar v loc) v loc
    -> Maybe
         (Constraint (UVar v loc) v loc, [UnsolvedConstraint v loc]))
-> Solve
     v
     loc
     (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc])
handleConstraint UVar v loc
s (Provenance v loc -> Constraint (UVar v loc) v loc
forall uv v loc. Provenance v loc -> Constraint uv v loc
Solved.IsAbility Provenance v loc
p0) \case
      Solved.IsAbility Provenance v loc
_ -> (Constraint (UVar v loc) v loc, [UnsolvedConstraint v loc])
-> Maybe
     (Constraint (UVar v loc) v loc, [UnsolvedConstraint v loc])
forall a. a -> Maybe a
Just (Provenance v loc -> Constraint (UVar v loc) v loc
forall uv v loc. Provenance v loc -> Constraint uv v loc
Solved.IsAbility Provenance v loc
p0, [])
      Constraint (UVar v loc) v loc
_ -> Maybe (Constraint (UVar v loc) v loc, [UnsolvedConstraint v loc])
forall a. Maybe a
Nothing
  Unsolved.IsType UVar v loc
s TypeProvenance v loc
p0 -> do
    UVar v loc
-> Constraint (UVar v loc) v loc
-> (Constraint (UVar v loc) v loc
    -> Maybe
         (Constraint (UVar v loc) v loc, [UnsolvedConstraint v loc]))
-> Solve
     v
     loc
     (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc])
handleConstraint UVar v loc
s (TypeProvenance v loc -> Constraint (UVar v loc) v loc
forall uv v loc. TypeProvenance v loc -> Constraint uv v loc
Solved.IsType TypeProvenance v loc
p0) \case
      Solved.IsType TypeProvenance v loc
_ -> (Constraint (UVar v loc) v loc, [UnsolvedConstraint v loc])
-> Maybe
     (Constraint (UVar v loc) v loc, [UnsolvedConstraint v loc])
forall a. a -> Maybe a
Just (TypeProvenance v loc -> Constraint (UVar v loc) v loc
forall uv v loc. TypeProvenance v loc -> Constraint uv v loc
Solved.IsType TypeProvenance v loc
p0, [])
      Constraint (UVar v loc) v loc
_ -> Maybe (Constraint (UVar v loc) v loc, [UnsolvedConstraint v loc])
forall a. Maybe a
Nothing
  Unsolved.IsArr UVar v loc
s Provenance v loc
p0 UVar v loc
a UVar v loc
b -> do
    -- If an @IsArr@ constraint is already present then we need to unify
    -- the left and right hand sides of the input constraints and the
    -- existing constraints, so we return those as implied constraints.
    UVar v loc
-> Constraint (UVar v loc) v loc
-> (Constraint (UVar v loc) v loc
    -> Maybe
         (Constraint (UVar v loc) v loc, [UnsolvedConstraint v loc]))
-> Solve
     v
     loc
     (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc])
handleConstraint UVar v loc
s (Provenance v loc
-> UVar v loc -> UVar v loc -> Constraint (UVar v loc) v loc
forall uv v loc.
Provenance v loc -> uv -> uv -> Constraint uv v loc
Solved.IsArr Provenance v loc
p0 UVar v loc
a UVar v loc
b) \case
      Solved.IsArr Provenance v loc
_p1 UVar v loc
c UVar v loc
d ->
        let implied :: [UnsolvedConstraint v loc]
implied =
              [ Provenance v loc
-> UVar v loc -> UVar v loc -> UnsolvedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
Provenance v loc -> uv -> uv -> Constraint uv v loc typeProv
Unsolved.Unify Provenance v loc
prov UVar v loc
a UVar v loc
c,
                Provenance v loc
-> UVar v loc -> UVar v loc -> UnsolvedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
Provenance v loc -> uv -> uv -> Constraint uv v loc typeProv
Unsolved.Unify Provenance v loc
prov UVar v loc
b UVar v loc
d
              ]
            prov :: Provenance v loc
prov = Provenance v loc
p0
         in (Constraint (UVar v loc) v loc, [UnsolvedConstraint v loc])
-> Maybe
     (Constraint (UVar v loc) v loc, [UnsolvedConstraint v loc])
forall a. a -> Maybe a
Just (Provenance v loc
-> UVar v loc -> UVar v loc -> Constraint (UVar v loc) v loc
forall uv v loc.
Provenance v loc -> uv -> uv -> Constraint uv v loc
Solved.IsArr Provenance v loc
prov UVar v loc
a UVar v loc
b, [UnsolvedConstraint v loc]
implied)
      Constraint (UVar v loc) v loc
_ -> Maybe (Constraint (UVar v loc) v loc, [UnsolvedConstraint v loc])
forall a. Maybe a
Nothing
  Unsolved.Unify Provenance v loc
l UVar v loc
a UVar v loc
b -> [UnsolvedConstraint v loc]
-> Either (ConstraintConflict v loc) [UnsolvedConstraint v loc]
forall a b. b -> Either a b
Right ([UnsolvedConstraint v loc]
 -> Either (ConstraintConflict v loc) [UnsolvedConstraint v loc])
-> Solve v loc [UnsolvedConstraint v loc]
-> Solve
     v
     loc
     (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Provenance v loc
-> UVar v loc
-> UVar v loc
-> Solve v loc [UnsolvedConstraint v loc]
forall loc v.
(Ord loc, Var v) =>
Provenance v loc
-> UVar v loc
-> UVar v loc
-> Solve v loc [UnsolvedConstraint v loc]
union Provenance v loc
l UVar v loc
a UVar v loc
b
  where
    -- \| A helper for solving various @Is*@ constraints. In each case
    -- we want to lookup any existing constraints on the constrained
    -- variable. If none exist then we simply add the new constraint,
    -- as it can't conflict with anything. If there is an existing
    -- constraint we defer to the passed in function.
    handleConstraint ::
      -- \| The variable mentioned in the input constraint
      UVar v loc ->
      -- \| The new constraint
      Solved.Constraint (UVar v loc) v loc ->
      -- \| How to handle the an existing constraint
      ( Solved.Constraint (UVar v loc) v loc ->
        Maybe (Solved.Constraint (UVar v loc) v loc, [UnsolvedConstraint v loc])
      ) ->
      -- \| An error or a list of implied constraints
      Solve v loc (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc])
    handleConstraint :: UVar v loc
-> Constraint (UVar v loc) v loc
-> (Constraint (UVar v loc) v loc
    -> Maybe
         (Constraint (UVar v loc) v loc, [UnsolvedConstraint v loc]))
-> Solve
     v
     loc
     (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc])
handleConstraint UVar v loc
s Constraint (UVar v loc) v loc
solvedConstraint Constraint (UVar v loc) v loc
-> Maybe
     (Constraint (UVar v loc) v loc, [UnsolvedConstraint v loc])
phi = do
      st :: SolveState v loc
st@SolveState {UFMap (UVar v loc) (Descriptor v loc)
$sel:constraints:SolveState :: forall v loc.
SolveState v loc -> UFMap (UVar v loc) (Descriptor v loc)
constraints :: UFMap (UVar v loc) (Descriptor v loc)
constraints} <- Solve v loc (SolveState v loc)
forall s (m :: * -> *). MonadState s m => m s
M.get
      let (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc]
postAction, UFMap (UVar v loc) (Descriptor v loc)
constraints') =
            UVar v loc
-> (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc],
    Maybe (Descriptor v loc))
-> (UVar v loc
    -> Int
    -> Descriptor v loc
    -> (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc],
        UFValue (UVar v loc) (Descriptor v loc)))
-> UFMap (UVar v loc) (Descriptor v loc)
-> (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc],
    UFMap (UVar v loc) (Descriptor v loc))
forall (f :: * -> *) k v.
(Functor f, Ord k) =>
k
-> f (Maybe v)
-> (k -> Int -> v -> f (UFValue k v))
-> UFMap k v
-> f (UFMap k v)
U.alterF
              UVar v loc
s
              ([Char]
-> (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc],
    Maybe (Descriptor v loc))
forall a. HasCallStack => [Char] -> a
error [Char]
"adding new uvar?")
              ( \UVar v loc
_canon Int
eqSize des :: Descriptor v loc
des@Descriptor {Maybe (Constraint (UVar v loc) v loc)
$sel:descriptorConstraint:Descriptor :: forall v loc.
Descriptor v loc -> Maybe (Constraint (UVar v loc) v loc)
descriptorConstraint :: Maybe (Constraint (UVar v loc) v loc)
descriptorConstraint} ->
                  let newDescriptor :: (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc],
 Descriptor v loc)
newDescriptor = case Maybe (Constraint (UVar v loc) v loc)
descriptorConstraint of
                        Maybe (Constraint (UVar v loc) v loc)
Nothing -> ([UnsolvedConstraint v loc]
-> Either (ConstraintConflict v loc) [UnsolvedConstraint v loc]
forall a b. b -> Either a b
Right [], Descriptor v loc
des {descriptorConstraint = Just solvedConstraint})
                        Just Constraint (UVar v loc) v loc
c1' -> case Constraint (UVar v loc) v loc
-> Maybe
     (Constraint (UVar v loc) v loc, [UnsolvedConstraint v loc])
phi Constraint (UVar v loc) v loc
c1' of
                          Just (Constraint (UVar v loc) v loc
newConstraint, [UnsolvedConstraint v loc]
impliedConstraints) ->
                            ([UnsolvedConstraint v loc]
-> Either (ConstraintConflict v loc) [UnsolvedConstraint v loc]
forall a b. b -> Either a b
Right [UnsolvedConstraint v loc]
impliedConstraints, Descriptor v loc
des {descriptorConstraint = Just newConstraint})
                          Maybe (Constraint (UVar v loc) v loc, [UnsolvedConstraint v loc])
Nothing ->
                            let conflict :: ConstraintConflict v loc
conflict =
                                  ConstraintConflict'
                                    { $sel:conflictedVar:ConstraintConflict' :: UVar v loc
conflictedVar = UVar v loc
s,
                                      $sel:impliedConstraint:ConstraintConflict' :: Constraint (UVar v loc) v loc
impliedConstraint = Constraint (UVar v loc) v loc
solvedConstraint,
                                      $sel:conflictedConstraint:ConstraintConflict' :: Constraint (UVar v loc) v loc
conflictedConstraint = Constraint (UVar v loc) v loc
c1'
                                    }
                             in (ConstraintConflict v loc
-> Either (ConstraintConflict v loc) [UnsolvedConstraint v loc]
forall a b. a -> Either a b
Left ConstraintConflict v loc
conflict, Descriptor v loc
des {descriptorConstraint = descriptorConstraint})
                   in Int -> Descriptor v loc -> UFValue (UVar v loc) (Descriptor v loc)
forall k v. Int -> v -> UFValue k v
U.Canonical Int
eqSize (Descriptor v loc -> UFValue (UVar v loc) (Descriptor v loc))
-> (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc],
    Descriptor v loc)
-> (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc],
    UFValue (UVar v loc) (Descriptor v loc))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Either (ConstraintConflict v loc) [UnsolvedConstraint v loc],
 Descriptor v loc)
newDescriptor
              )
              UFMap (UVar v loc) (Descriptor v loc)
constraints
      SolveState v loc -> Solve v loc ()
forall s (m :: * -> *). MonadState s m => s -> m ()
M.put SolveState v loc
st {constraints = constraints'}
      pure Either (ConstraintConflict v loc) [UnsolvedConstraint v loc]
postAction

-- unify two uvars, returning implied constraints
union :: (Ord loc, Var v) => Provenance v loc -> UVar v loc -> UVar v loc -> Solve v loc [UnsolvedConstraint v loc]
union :: forall loc v.
(Ord loc, Var v) =>
Provenance v loc
-> UVar v loc
-> UVar v loc
-> Solve v loc [UnsolvedConstraint v loc]
union Provenance v loc
_unionLoc UVar v loc
a UVar v loc
b = do
  SolveState {UFMap (UVar v loc) (Descriptor v loc)
$sel:constraints:SolveState :: forall v loc.
SolveState v loc -> UFMap (UVar v loc) (Descriptor v loc)
constraints :: UFMap (UVar v loc) (Descriptor v loc)
constraints} <- Solve v loc (SolveState v loc)
forall s (m :: * -> *). MonadState s m => m s
M.get
  Maybe [UnsolvedConstraint v loc]
res <- UVar v loc
-> UVar v loc
-> UFMap (UVar v loc) (Descriptor v loc)
-> (UFMap (UVar v loc) (Descriptor v loc)
    -> Solve v loc [UnsolvedConstraint v loc])
-> (UVar v loc
    -> Descriptor v loc
    -> UFMap (UVar v loc) (Descriptor v loc)
    -> Solve v loc (Maybe [UnsolvedConstraint v loc]))
-> Solve v loc (Maybe [UnsolvedConstraint v loc])
forall (m :: * -> *) k v r.
(MonadFix m, Ord k) =>
k
-> k
-> UFMap k v
-> (UFMap k v -> m r)
-> (k -> v -> UFMap k v -> m (Maybe r))
-> m (Maybe r)
U.union UVar v loc
a UVar v loc
b UFMap (UVar v loc) (Descriptor v loc)
constraints UFMap (UVar v loc) (Descriptor v loc)
-> Solve v loc [UnsolvedConstraint v loc]
forall {m :: * -> *} {v} {loc} {a}.
MonadState (SolveState v loc) m =>
UFMap (UVar v loc) (Descriptor v loc) -> m [a]
noMerge \UVar v loc
_canonK Descriptor v loc
nonCanonV UFMap (UVar v loc) (Descriptor v loc)
constraints' -> do
    SolveState v loc
st <- Solve v loc (SolveState v loc)
forall s (m :: * -> *). MonadState s m => m s
M.get
    SolveState v loc -> Solve v loc ()
forall s (m :: * -> *). MonadState s m => s -> m ()
M.put SolveState v loc
st {constraints = constraints'}
    let impliedConstraints :: [UnsolvedConstraint v loc]
impliedConstraints = case Descriptor v loc -> Maybe (Constraint (UVar v loc) v loc)
forall v loc.
Descriptor v loc -> Maybe (Constraint (UVar v loc) v loc)
descriptorConstraint Descriptor v loc
nonCanonV of
          Maybe (Constraint (UVar v loc) v loc)
Nothing -> []
          Just Constraint (UVar v loc) v loc
c ->
            let cd :: UnsolvedConstraint v loc
cd = case Constraint (UVar v loc) v loc
c of
                  Solved.IsType TypeProvenance v loc
loc -> UVar v loc -> TypeProvenance v loc -> UnsolvedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
uv -> typeProv v loc -> Constraint uv v loc typeProv
Unsolved.IsType UVar v loc
a case TypeProvenance v loc
loc of
                    TypeProvenance v loc
Default -> TypeProvenance v loc
forall v loc. TypeProvenance v loc
Default
                    NotDefault Provenance v loc
loc -> Provenance v loc -> TypeProvenance v loc
forall v loc. Provenance v loc -> TypeProvenance v loc
NotDefault Provenance v loc
loc
                  Solved.IsArr Provenance v loc
loc UVar v loc
l UVar v loc
r -> UVar v loc
-> Provenance v loc
-> UVar v loc
-> UVar v loc
-> UnsolvedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
uv -> Provenance v loc -> uv -> uv -> Constraint uv v loc typeProv
Unsolved.IsArr UVar v loc
a Provenance v loc
loc UVar v loc
l UVar v loc
r
                  Solved.IsAbility Provenance v loc
loc -> UVar v loc -> Provenance v loc -> UnsolvedConstraint v loc
forall uv v loc (typeProv :: * -> * -> *).
uv -> Provenance v loc -> Constraint uv v loc typeProv
Unsolved.IsAbility UVar v loc
a Provenance v loc
loc
             in [UnsolvedConstraint v loc
cd]
    pure ([UnsolvedConstraint v loc] -> Maybe [UnsolvedConstraint v loc]
forall a. a -> Maybe a
Just [UnsolvedConstraint v loc]
impliedConstraints)

  case Maybe [UnsolvedConstraint v loc]
res of
    Maybe [UnsolvedConstraint v loc]
Nothing -> [Char] -> Solve v loc [UnsolvedConstraint v loc]
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible"
    Just [UnsolvedConstraint v loc]
impliedConstraints -> [UnsolvedConstraint v loc]
-> Solve v loc [UnsolvedConstraint v loc]
forall a. a -> Solve v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [UnsolvedConstraint v loc]
impliedConstraints
  where
    noMerge :: UFMap (UVar v loc) (Descriptor v loc) -> m [a]
noMerge UFMap (UVar v loc) (Descriptor v loc)
m = do
      SolveState v loc
st <- m (SolveState v loc)
forall s (m :: * -> *). MonadState s m => m s
M.get
      SolveState v loc -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
M.put SolveState v loc
st {constraints = m}
      pure []

-- | Do an occurence check and return an error or the resulting solve
-- state
verify ::
  (Var v) =>
  SolveState v loc ->
  Either (NonEmpty (KindError v loc)) (SolveState v loc)
verify :: forall v loc.
Var v =>
SolveState v loc
-> Either (NonEmpty (KindError v loc)) (SolveState v loc)
verify SolveState v loc
st =
  let solveState :: Either (NonEmpty (KindError v loc)) (ConstraintMap v loc)
solveState = ConstraintMap v loc
-> Either (NonEmpty (KindError v loc)) (ConstraintMap v loc)
forall v loc.
Var v =>
ConstraintMap v loc
-> Either (NonEmpty (KindError v loc)) (ConstraintMap v loc)
occCheck (SolveState v loc -> ConstraintMap v loc
forall v loc.
SolveState v loc -> UFMap (UVar v loc) (Descriptor v loc)
constraints SolveState v loc
st)
   in case Either (NonEmpty (KindError v loc)) (ConstraintMap v loc)
solveState of
        Left NonEmpty (KindError v loc)
e -> NonEmpty (KindError v loc)
-> Either (NonEmpty (KindError v loc)) (SolveState v loc)
forall a b. a -> Either a b
Left NonEmpty (KindError v loc)
e
        Right ConstraintMap v loc
m -> SolveState v loc
-> Either (NonEmpty (KindError v loc)) (SolveState v loc)
forall a b. b -> Either a b
Right SolveState v loc
st {constraints = m}

--------------------------------------------------------------------------------
-- @SolveState@ initialization
--------------------------------------------------------------------------------

initialState :: forall v loc. (BuiltinAnnotation loc, Show loc, Ord loc, Var v) => Env -> SolveState v loc
initialState :: forall v loc.
(BuiltinAnnotation loc, Show loc, Ord loc, Var v) =>
Env -> SolveState v loc
initialState Env
env =
  let ((), SolveState v loc
finalState) = Env -> SolveState v loc -> Solve v loc () -> ((), SolveState v loc)
forall v loc a.
Env -> SolveState v loc -> Solve v loc a -> (a, SolveState v loc)
run Env
env SolveState v loc
forall v loc. SolveState v loc
emptyState Solve v loc ()
forall v loc.
(BuiltinAnnotation loc, Ord loc, Show loc, Var v) =>
Solve v loc ()
initializeState
   in SolveState v loc
finalState

initializeState :: forall v loc. (BuiltinAnnotation loc, Ord loc, Show loc, Var v) => Solve v loc ()
initializeState :: forall v loc.
(BuiltinAnnotation loc, Ord loc, Show loc, Var v) =>
Solve v loc ()
initializeState = Gen v loc [GeneratedConstraint v loc] -> Solve v loc ()
forall loc v.
(Ord loc, Show loc, Var v) =>
Gen v loc [GeneratedConstraint v loc] -> Solve v loc ()
assertGen do
  Gen v loc [GeneratedConstraint v loc]
forall v loc.
(Ord loc, BuiltinAnnotation loc, Var v) =>
Gen v loc [GeneratedConstraint v loc]
builtinConstraints

-- | Generate and solve constraints, asserting no conflicts or
-- decomposition occurs
assertGen :: (Ord loc, Show loc, Var v) => Gen v loc [GeneratedConstraint v loc] -> Solve v loc ()
assertGen :: forall loc v.
(Ord loc, Show loc, Var v) =>
Gen v loc [GeneratedConstraint v loc] -> Solve v loc ()
assertGen Gen v loc [GeneratedConstraint v loc]
gen = do
  [GeneratedConstraint v loc]
cs <- Gen v loc [GeneratedConstraint v loc]
-> Solve v loc [GeneratedConstraint v loc]
forall v loc a. Var v => Gen v loc a -> Solve v loc a
runGen Gen v loc [GeneratedConstraint v loc]
gen
  Env
env <- Solve v loc Env
forall r (m :: * -> *). MonadReader r m => m r
M.ask
  SolveState v loc
st <- Solve v loc (SolveState v loc)
forall s (m :: * -> *). MonadState s m => m s
M.get
  let comp :: Either (NonEmpty (KindError v loc)) (SolveState v loc)
comp = do
        SolveState v loc
st <- Env
-> SolveState v loc
-> [GeneratedConstraint v loc]
-> Either (NonEmpty (KindError v loc)) (SolveState v loc)
forall v loc.
(Var v, Ord loc, Show loc) =>
Env
-> SolveState v loc
-> [GeneratedConstraint v loc]
-> Either (NonEmpty (KindError v loc)) (SolveState v loc)
step Env
env SolveState v loc
st [GeneratedConstraint v loc]
cs
        SolveState v loc
-> Either (NonEmpty (KindError v loc)) (SolveState v loc)
forall v loc.
Var v =>
SolveState v loc
-> Either (NonEmpty (KindError v loc)) (SolveState v loc)
verify SolveState v loc
st
  case Either (NonEmpty (KindError v loc)) (SolveState v loc)
comp of
    Left NonEmpty (KindError v loc)
_ -> [Char] -> Solve v loc ()
forall a. HasCallStack => [Char] -> a
error [Char]
"[assertGen]: constraint failure in builtin constraints"
    Right SolveState v loc
st -> SolveState v loc -> Solve v loc ()
forall s (m :: * -> *). MonadState s m => s -> m ()
M.put SolveState v loc
st

--------------------------------------------------------------------------------
-- Occurence check and helpers
--------------------------------------------------------------------------------

-- | occurence check and report any errors
occCheck ::
  forall v loc.
  (Var v) =>
  ConstraintMap v loc ->
  Either (NonEmpty (KindError v loc)) (ConstraintMap v loc)
occCheck :: forall v loc.
Var v =>
ConstraintMap v loc
-> Either (NonEmpty (KindError v loc)) (ConstraintMap v loc)
occCheck ConstraintMap v loc
constraints0 =
  let go ::
        [(UVar v loc)] ->
        M.State (OccCheckState v loc) ()
      go :: [UVar v loc] -> State (OccCheckState v loc) ()
go = \case
        [] -> () -> State (OccCheckState v loc) ()
forall a. a -> StateT (OccCheckState v loc) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        UVar v loc
u : [UVar v loc]
us -> do
          UVar v loc -> State (OccCheckState v loc) Bool
forall v loc.
Var v =>
UVar v loc -> State (OccCheckState v loc) Bool
isSolved UVar v loc
u State (OccCheckState v loc) Bool
-> (Bool -> State (OccCheckState v loc) ())
-> State (OccCheckState v loc) ()
forall a b.
StateT (OccCheckState v loc) Identity a
-> (a -> StateT (OccCheckState v loc) Identity b)
-> StateT (OccCheckState v loc) Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Bool
True -> [UVar v loc] -> State (OccCheckState v loc) ()
go [UVar v loc]
us
            Bool
False -> do
              UVar v loc -> State (OccCheckState v loc) CycleCheck
forall v loc.
Var v =>
UVar v loc -> State (OccCheckState v loc) CycleCheck
markVisiting UVar v loc
u State (OccCheckState v loc) CycleCheck
-> (CycleCheck -> State (OccCheckState v loc) ())
-> State (OccCheckState v loc) ()
forall a b.
StateT (OccCheckState v loc) Identity a
-> (a -> StateT (OccCheckState v loc) Identity b)
-> StateT (OccCheckState v loc) Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                CycleCheck
Cycle -> () -> State (OccCheckState v loc) ()
forall a. a -> StateT (OccCheckState v loc) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                CycleCheck
NoCycle -> do
                  st :: OccCheckState v loc
st@OccCheckState {ConstraintMap v loc
solvedConstraints :: ConstraintMap v loc
$sel:solvedConstraints:OccCheckState :: forall v loc. OccCheckState v loc -> ConstraintMap v loc
solvedConstraints} <- StateT (OccCheckState v loc) Identity (OccCheckState v loc)
forall s (m :: * -> *). MonadState s m => m s
M.get
                  let handleNothing :: a
handleNothing = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible"
                      handleJust :: p
-> Int
-> Descriptor v loc
-> ([UVar v loc], UFValue k (Descriptor v loc))
handleJust p
_canonK Int
ecSize Descriptor v loc
d = case Descriptor v loc -> Maybe (Constraint (UVar v loc) v loc)
forall v loc.
Descriptor v loc -> Maybe (Constraint (UVar v loc) v loc)
descriptorConstraint Descriptor v loc
d of
                        Maybe (Constraint (UVar v loc) v loc)
Nothing -> ([], Int -> Descriptor v loc -> UFValue k (Descriptor v loc)
forall k v. Int -> v -> UFValue k v
U.Canonical Int
ecSize Descriptor v loc
d {descriptorConstraint = Just $ Solved.IsType Default})
                        Just Constraint (UVar v loc) v loc
v ->
                          let descendants :: [UVar v loc]
descendants = case Constraint (UVar v loc) v loc
v of
                                Solved.IsType TypeProvenance v loc
_ -> []
                                Solved.IsAbility Provenance v loc
_ -> []
                                Solved.IsArr Provenance v loc
_ UVar v loc
a UVar v loc
b -> [UVar v loc
a, UVar v loc
b]
                           in ([UVar v loc]
descendants, Int -> Descriptor v loc -> UFValue k (Descriptor v loc)
forall k v. Int -> v -> UFValue k v
U.Canonical Int
ecSize Descriptor v loc
d)
                  let ([UVar v loc]
descendants, ConstraintMap v loc
solvedConstraints') = UVar v loc
-> ([UVar v loc], Maybe (Descriptor v loc))
-> (UVar v loc
    -> Int
    -> Descriptor v loc
    -> ([UVar v loc], UFValue (UVar v loc) (Descriptor v loc)))
-> ConstraintMap v loc
-> ([UVar v loc], ConstraintMap v loc)
forall (f :: * -> *) k v.
(Functor f, Ord k) =>
k
-> f (Maybe v)
-> (k -> Int -> v -> f (UFValue k v))
-> UFMap k v
-> f (UFMap k v)
U.alterF UVar v loc
u ([UVar v loc], Maybe (Descriptor v loc))
forall {a}. a
handleNothing UVar v loc
-> Int
-> Descriptor v loc
-> ([UVar v loc], UFValue (UVar v loc) (Descriptor v loc))
forall {p} {v} {loc} {k}.
p
-> Int
-> Descriptor v loc
-> ([UVar v loc], UFValue k (Descriptor v loc))
handleJust ConstraintMap v loc
solvedConstraints
                  OccCheckState v loc -> State (OccCheckState v loc) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
M.put OccCheckState v loc
st {solvedConstraints = solvedConstraints'}
                  [UVar v loc] -> State (OccCheckState v loc) ()
go [UVar v loc]
descendants
              UVar v loc -> State (OccCheckState v loc) ()
forall v loc. Var v => UVar v loc -> State (OccCheckState v loc) ()
unmarkVisiting UVar v loc
u
              [UVar v loc] -> State (OccCheckState v loc) ()
go [UVar v loc]
us

      OccCheckState {ConstraintMap v loc
$sel:solvedConstraints:OccCheckState :: forall v loc. OccCheckState v loc -> ConstraintMap v loc
solvedConstraints :: ConstraintMap v loc
solvedConstraints, [KindError v loc]
kindErrors :: [KindError v loc]
$sel:kindErrors:OccCheckState :: forall v loc. OccCheckState v loc -> [KindError v loc]
kindErrors} =
        State (OccCheckState v loc) ()
-> OccCheckState v loc -> OccCheckState v loc
forall s a. State s a -> s -> s
M.execState
          ([UVar v loc] -> State (OccCheckState v loc) ()
go (ConstraintMap v loc -> [UVar v loc]
forall k v. UFMap k v -> [k]
U.keys ConstraintMap v loc
constraints0))
          OccCheckState
            { $sel:visitingSet:OccCheckState :: Set (UVar v loc)
visitingSet = Set (UVar v loc)
forall a. Set a
Set.empty,
              $sel:visitingStack:OccCheckState :: [UVar v loc]
visitingStack = [],
              $sel:solvedSet:OccCheckState :: Set (UVar v loc)
solvedSet = Set (UVar v loc)
forall a. Set a
Set.empty,
              $sel:solvedConstraints:OccCheckState :: ConstraintMap v loc
solvedConstraints = ConstraintMap v loc
constraints0,
              $sel:kindErrors:OccCheckState :: [KindError v loc]
kindErrors = []
            }
   in case [KindError v loc]
kindErrors of
        [] -> ConstraintMap v loc
-> Either (NonEmpty (KindError v loc)) (ConstraintMap v loc)
forall a b. b -> Either a b
Right ConstraintMap v loc
solvedConstraints
        KindError v loc
e : [KindError v loc]
es -> NonEmpty (KindError v loc)
-> Either (NonEmpty (KindError v loc)) (ConstraintMap v loc)
forall a b. a -> Either a b
Left (KindError v loc
e KindError v loc -> [KindError v loc] -> NonEmpty (KindError v loc)
forall a. a -> [a] -> NonEmpty a
:| [KindError v loc]
es)

data OccCheckState v loc = OccCheckState
  { forall v loc. OccCheckState v loc -> Set (UVar v loc)
visitingSet :: Set (UVar v loc),
    forall v loc. OccCheckState v loc -> [UVar v loc]
visitingStack :: [UVar v loc],
    forall v loc. OccCheckState v loc -> Set (UVar v loc)
solvedSet :: Set (UVar v loc),
    forall v loc. OccCheckState v loc -> ConstraintMap v loc
solvedConstraints :: ConstraintMap v loc,
    forall v loc. OccCheckState v loc -> [KindError v loc]
kindErrors :: [KindError v loc]
  }

markVisiting :: (Var v) => UVar v loc -> M.State (OccCheckState v loc) CycleCheck
markVisiting :: forall v loc.
Var v =>
UVar v loc -> State (OccCheckState v loc) CycleCheck
markVisiting UVar v loc
x = do
  OccCheckState {Set (UVar v loc)
$sel:visitingSet:OccCheckState :: forall v loc. OccCheckState v loc -> Set (UVar v loc)
visitingSet :: Set (UVar v loc)
visitingSet, [UVar v loc]
$sel:visitingStack:OccCheckState :: forall v loc. OccCheckState v loc -> [UVar v loc]
visitingStack :: [UVar v loc]
visitingStack} <- StateT (OccCheckState v loc) Identity (OccCheckState v loc)
forall s (m :: * -> *). MonadState s m => m s
M.get
  case UVar v loc -> Set (UVar v loc) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member UVar v loc
x Set (UVar v loc)
visitingSet of
    Bool
True -> do
      OccCheckState {ConstraintMap v loc
$sel:solvedConstraints:OccCheckState :: forall v loc. OccCheckState v loc -> ConstraintMap v loc
solvedConstraints :: ConstraintMap v loc
solvedConstraints} <- StateT (OccCheckState v loc) Identity (OccCheckState v loc)
forall s (m :: * -> *). MonadState s m => m s
M.get
      let loc :: loc
loc = case UVar v loc
-> ConstraintMap v loc
-> Maybe (UVar v loc, Int, Descriptor v loc, ConstraintMap v loc)
forall k v. Ord k => k -> UFMap k v -> Maybe (k, Int, v, UFMap k v)
U.lookupCanon UVar v loc
x ConstraintMap v loc
solvedConstraints of
            Just (UVar v loc
_, Int
_, Descriptor {$sel:descriptorConstraint:Descriptor :: forall v loc.
Descriptor v loc -> Maybe (Constraint (UVar v loc) v loc)
descriptorConstraint = Just (Solved.IsArr (Provenance ConstraintContext v loc
_ loc
loc) UVar v loc
_ UVar v loc
_)}, ConstraintMap v loc
_) -> loc
loc
            Maybe (UVar v loc, Int, Descriptor v loc, ConstraintMap v loc)
_ -> [Char] -> loc
forall a. HasCallStack => [Char] -> a
error [Char]
"cycle without IsArr constraint"
      KindError v loc -> State (OccCheckState v loc) ()
forall v loc. KindError v loc -> State (OccCheckState v loc) ()
addError (loc -> UVar v loc -> ConstraintMap v loc -> KindError v loc
forall v loc.
loc -> UVar v loc -> ConstraintMap v loc -> KindError v loc
CycleDetected loc
loc UVar v loc
x ConstraintMap v loc
solvedConstraints)
      pure CycleCheck
Cycle
    Bool
False -> do
      (OccCheckState v loc -> OccCheckState v loc)
-> State (OccCheckState v loc) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
M.modify \OccCheckState v loc
st ->
        OccCheckState v loc
st
          { visitingSet = Set.insert x visitingSet,
            visitingStack = x : visitingStack
          }
      pure CycleCheck
NoCycle

unmarkVisiting :: (Var v) => UVar v loc -> M.State (OccCheckState v loc) ()
unmarkVisiting :: forall v loc. Var v => UVar v loc -> State (OccCheckState v loc) ()
unmarkVisiting UVar v loc
x = (OccCheckState v loc -> OccCheckState v loc)
-> StateT (OccCheckState v loc) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
M.modify \OccCheckState v loc
st ->
  OccCheckState v loc
st
    { visitingSet = Set.delete x (visitingSet st),
      visitingStack = tail (visitingStack st),
      solvedSet = Set.insert x (solvedSet st)
    }

addError :: KindError v loc -> M.State (OccCheckState v loc) ()
addError :: forall v loc. KindError v loc -> State (OccCheckState v loc) ()
addError KindError v loc
ke = (OccCheckState v loc -> OccCheckState v loc)
-> StateT (OccCheckState v loc) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
M.modify \OccCheckState v loc
st -> OccCheckState v loc
st {kindErrors = ke : kindErrors st}

isSolved :: (Var v) => UVar v loc -> M.State (OccCheckState v loc) Bool
isSolved :: forall v loc.
Var v =>
UVar v loc -> State (OccCheckState v loc) Bool
isSolved UVar v loc
x = do
  OccCheckState {Set (UVar v loc)
$sel:solvedSet:OccCheckState :: forall v loc. OccCheckState v loc -> Set (UVar v loc)
solvedSet :: Set (UVar v loc)
solvedSet} <- StateT (OccCheckState v loc) Identity (OccCheckState v loc)
forall s (m :: * -> *). MonadState s m => m s
M.get
  Bool -> State (OccCheckState v loc) Bool
forall a. a -> StateT (OccCheckState v loc) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> State (OccCheckState v loc) Bool)
-> Bool -> State (OccCheckState v loc) Bool
forall a b. (a -> b) -> a -> b
$ UVar v loc -> Set (UVar v loc) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member UVar v loc
x Set (UVar v loc)
solvedSet

data CycleCheck
  = Cycle
  | NoCycle

--------------------------------------------------------------------------------
-- Debug output helpers
--------------------------------------------------------------------------------

prettyConstraintD' :: (Show loc, Var v) => PrettyPrintEnv -> UnsolvedConstraint v loc -> P.Pretty P.ColorText
prettyConstraintD' :: forall loc v.
(Show loc, Var v) =>
PrettyPrintEnv -> UnsolvedConstraint v loc -> Pretty ColorText
prettyConstraintD' PrettyPrintEnv
ppe =
  Pretty ColorText -> Pretty ColorText
forall s. (ListLike s Char, IsString s) => Pretty s -> Pretty s
P.wrap (Pretty ColorText -> Pretty ColorText)
-> (UnsolvedConstraint v loc -> Pretty ColorText)
-> UnsolvedConstraint v loc
-> Pretty ColorText
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
    Unsolved.IsType UVar v loc
v TypeProvenance v loc
p -> PrettyPrintEnv -> UVar v loc -> Pretty ColorText
forall v loc.
Var v =>
PrettyPrintEnv -> UVar v loc -> Pretty ColorText
prettyUVar PrettyPrintEnv
ppe UVar v loc
v Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall a. Semigroup a => a -> a -> a
<> Pretty ColorText
" ~ Type" Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall a. Semigroup a => a -> a -> a
<> TypeProvenance v loc -> Pretty ColorText
forall {s} {a}. (IsString s, Show a) => a -> Pretty s
prettyProv TypeProvenance v loc
p
    Unsolved.IsAbility UVar v loc
v Provenance v loc
p -> PrettyPrintEnv -> UVar v loc -> Pretty ColorText
forall v loc.
Var v =>
PrettyPrintEnv -> UVar v loc -> Pretty ColorText
prettyUVar PrettyPrintEnv
ppe UVar v loc
v Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall a. Semigroup a => a -> a -> a
<> Pretty ColorText
" ~ Ability" Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall a. Semigroup a => a -> a -> a
<> Provenance v loc -> Pretty ColorText
forall {s} {a}. (IsString s, Show a) => a -> Pretty s
prettyProv Provenance v loc
p
    Unsolved.IsArr UVar v loc
v Provenance v loc
p UVar v loc
a UVar v loc
b -> PrettyPrintEnv -> UVar v loc -> Pretty ColorText
forall v loc.
Var v =>
PrettyPrintEnv -> UVar v loc -> Pretty ColorText
prettyUVar PrettyPrintEnv
ppe UVar v loc
v Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall a. Semigroup a => a -> a -> a
<> Pretty ColorText
" ~ " Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall a. Semigroup a => a -> a -> a
<> PrettyPrintEnv -> UVar v loc -> Pretty ColorText
forall v loc.
Var v =>
PrettyPrintEnv -> UVar v loc -> Pretty ColorText
prettyUVar PrettyPrintEnv
ppe UVar v loc
a Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall a. Semigroup a => a -> a -> a
<> Pretty ColorText
" -> " Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall a. Semigroup a => a -> a -> a
<> PrettyPrintEnv -> UVar v loc -> Pretty ColorText
forall v loc.
Var v =>
PrettyPrintEnv -> UVar v loc -> Pretty ColorText
prettyUVar PrettyPrintEnv
ppe UVar v loc
b Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall a. Semigroup a => a -> a -> a
<> Provenance v loc -> Pretty ColorText
forall {s} {a}. (IsString s, Show a) => a -> Pretty s
prettyProv Provenance v loc
p
    Unsolved.Unify Provenance v loc
p UVar v loc
a UVar v loc
b -> PrettyPrintEnv -> UVar v loc -> Pretty ColorText
forall v loc.
Var v =>
PrettyPrintEnv -> UVar v loc -> Pretty ColorText
prettyUVar PrettyPrintEnv
ppe UVar v loc
a Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall a. Semigroup a => a -> a -> a
<> Pretty ColorText
" ~ " Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall a. Semigroup a => a -> a -> a
<> PrettyPrintEnv -> UVar v loc -> Pretty ColorText
forall v loc.
Var v =>
PrettyPrintEnv -> UVar v loc -> Pretty ColorText
prettyUVar PrettyPrintEnv
ppe UVar v loc
b Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall a. Semigroup a => a -> a -> a
<> Provenance v loc -> Pretty ColorText
forall {s} {a}. (IsString s, Show a) => a -> Pretty s
prettyProv Provenance v loc
p
  where
    prettyProv :: a -> Pretty s
prettyProv a
x =
      Pretty s
"[" Pretty s -> Pretty s -> Pretty s
forall a. Semigroup a => a -> a -> a
<> [Char] -> Pretty s
forall s. IsString s => [Char] -> Pretty s
P.string (a -> [Char]
forall a. Show a => a -> [Char]
show a
x) Pretty s -> Pretty s -> Pretty s
forall a. Semigroup a => a -> a -> a
<> Pretty s
"]"

prettyConstraints :: (Show loc, Var v) => PrettyPrintEnv -> [UnsolvedConstraint v loc] -> P.Pretty P.ColorText
prettyConstraints :: forall loc v.
(Show loc, Var v) =>
PrettyPrintEnv -> [UnsolvedConstraint v loc] -> Pretty ColorText
prettyConstraints PrettyPrintEnv
ppe = Pretty ColorText -> [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
Pretty s -> f (Pretty s) -> Pretty s
P.sep Pretty ColorText
"\n" ([Pretty ColorText] -> Pretty ColorText)
-> ([UnsolvedConstraint v loc] -> [Pretty ColorText])
-> [UnsolvedConstraint v loc]
-> Pretty ColorText
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UnsolvedConstraint v loc -> Pretty ColorText)
-> [UnsolvedConstraint v loc] -> [Pretty ColorText]
forall a b. (a -> b) -> [a] -> [b]
map (PrettyPrintEnv -> UnsolvedConstraint v loc -> Pretty ColorText
forall loc v.
(Show loc, Var v) =>
PrettyPrintEnv -> UnsolvedConstraint v loc -> Pretty ColorText
prettyConstraintD' PrettyPrintEnv
ppe)

prettyUVar :: (Var v) => PrettyPrintEnv -> UVar v loc -> P.Pretty P.ColorText
prettyUVar :: forall v loc.
Var v =>
PrettyPrintEnv -> UVar v loc -> Pretty ColorText
prettyUVar PrettyPrintEnv
ppe (UVar Symbol
s Type v loc
t) = PrettyPrintEnv -> Type v loc -> Pretty ColorText
forall v a. Var v => PrettyPrintEnv -> Type v a -> Pretty ColorText
TP.pretty PrettyPrintEnv
ppe Type v loc
t Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall a. Semigroup a => a -> a -> a
<> Pretty ColorText
" :: " Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall a. Semigroup a => a -> a -> a
<> Symbol -> Pretty ColorText
forall v. Var v => v -> Pretty ColorText
P.prettyVar Symbol
s

tracePretty :: P.Pretty P.ColorText -> a -> a
tracePretty :: forall a. Pretty ColorText -> a -> a
tracePretty Pretty ColorText
p = [Char] -> a -> a
forall a. [Char] -> a -> a
trace (Pretty ColorText -> [Char]
P.toAnsiUnbroken Pretty ColorText
p)