{-# LANGUAGE RecursiveDo #-}

-- | Description: Pretty printers for kind inference constraints
module Unison.KindInference.Constraint.Pretty
  ( prettyUVarKind,
    prettySolvedConstraint,
    tryPrettySolvedConstraint,
    tryPrettyUVarKind,
    prettyCyclicUVarKind,
    prettySolveError,
  )
where

import Data.Map qualified as Map
import Data.Set qualified as Set
import Unison.KindInference.Constraint.Solved qualified as Solved
import Unison.KindInference.Solve.Monad
  ( ConstraintMap,
    Env (..),
    Solve (..),
    SolveError (..),
    SolveState (..),
    find,
    runSolve,
  )
import Unison.KindInference.UVar (UVar (..))
import Unison.Prelude
import Unison.PrettyPrintEnv (PrettyPrintEnv)
import Unison.Util.Pretty qualified as P
import Unison.Var (Var)

arrPrec :: Int
arrPrec :: Int
arrPrec = Int
1

prettyAbility :: Int -> P.Pretty P.ColorText
prettyAbility :: Int -> Pretty ColorText
prettyAbility Int
_prec = Pretty ColorText
"Ability"

prettyType :: Int -> P.Pretty P.ColorText
prettyType :: Int -> Pretty ColorText
prettyType Int
_prec = Pretty ColorText
"Type"

prettyUnknown :: Int -> P.Pretty P.ColorText
prettyUnknown :: Int -> Pretty ColorText
prettyUnknown Int
_prec = Pretty ColorText
"_"

prettyArrow :: Int -> P.Pretty P.ColorText -> P.Pretty P.ColorText -> P.Pretty P.ColorText
prettyArrow :: Int -> Pretty ColorText -> Pretty ColorText -> Pretty ColorText
prettyArrow Int
prec Pretty ColorText
lhs Pretty ColorText
rhs =
  let wrap :: Pretty ColorText -> Pretty ColorText
wrap = if Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
arrPrec then Pretty ColorText -> Pretty ColorText
forall s. IsString s => Pretty s -> Pretty s
P.parenthesize else Pretty ColorText -> Pretty ColorText
forall a. a -> a
id
   in Pretty ColorText -> Pretty ColorText
wrap (Pretty ColorText
lhs 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
<> Pretty ColorText
rhs)

prettyCyclicSolvedConstraint ::
  (Var v) =>
  Solved.Constraint (UVar v loc) v loc ->
  Int ->
  Map (UVar v loc) (P.Pretty P.ColorText) ->
  Set (UVar v loc) ->
  Solve v loc (P.Pretty P.ColorText, Set (UVar v loc))
prettyCyclicSolvedConstraint :: forall v loc.
Var v =>
Constraint (UVar v loc) v loc
-> Int
-> Map (UVar v loc) (Pretty ColorText)
-> Set (UVar v loc)
-> Solve v loc (Pretty ColorText, Set (UVar v loc))
prettyCyclicSolvedConstraint Constraint (UVar v loc) v loc
constraint Int
prec Map (UVar v loc) (Pretty ColorText)
nameMap Set (UVar v loc)
visitingSet = case Constraint (UVar v loc) v loc
constraint of
  Solved.IsAbility Provenance v loc
_ -> (Pretty ColorText, Set (UVar v loc))
-> Solve v loc (Pretty ColorText, Set (UVar v loc))
forall a. a -> Solve v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Pretty ColorText
prettyAbility Int
prec, Set (UVar v loc)
forall a. Set a
Set.empty)
  Solved.IsType TypeProvenance v loc
_ -> (Pretty ColorText, Set (UVar v loc))
-> Solve v loc (Pretty ColorText, Set (UVar v loc))
forall a. a -> Solve v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Pretty ColorText
prettyType Int
prec, Set (UVar v loc)
forall a. Set a
Set.empty)
  Solved.IsArr Provenance v loc
_ UVar v loc
a UVar v loc
b -> do
    (Pretty ColorText
pa, Set (UVar v loc)
cyclicLhs) <- case UVar v loc -> Set (UVar v loc) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member UVar v loc
a Set (UVar v loc)
visitingSet of
      Bool
True -> (Pretty ColorText, Set (UVar v loc))
-> Solve v loc (Pretty ColorText, Set (UVar v loc))
forall a. a -> Solve v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map (UVar v loc) (Pretty ColorText)
nameMap Map (UVar v loc) (Pretty ColorText)
-> UVar v loc -> Pretty ColorText
forall k a. Ord k => Map k a -> k -> a
Map.! UVar v loc
a, UVar v loc -> Set (UVar v loc)
forall a. a -> Set a
Set.singleton UVar v loc
a)
      Bool
False -> Int
-> UVar v loc
-> Map (UVar v loc) (Pretty ColorText)
-> Set (UVar v loc)
-> Solve v loc (Pretty ColorText, Set (UVar v loc))
forall v loc.
Var v =>
Int
-> UVar v loc
-> Map (UVar v loc) (Pretty ColorText)
-> Set (UVar v loc)
-> Solve v loc (Pretty ColorText, Set (UVar v loc))
prettyCyclicUVarKindWorker (Int
arrPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) UVar v loc
a Map (UVar v loc) (Pretty ColorText)
nameMap Set (UVar v loc)
visitingSet
    (Pretty ColorText
pb, Set (UVar v loc)
cyclicRhs) <- case UVar v loc -> Set (UVar v loc) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member UVar v loc
b Set (UVar v loc)
visitingSet of
      Bool
True -> (Pretty ColorText, Set (UVar v loc))
-> Solve v loc (Pretty ColorText, Set (UVar v loc))
forall a. a -> Solve v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map (UVar v loc) (Pretty ColorText)
nameMap Map (UVar v loc) (Pretty ColorText)
-> UVar v loc -> Pretty ColorText
forall k a. Ord k => Map k a -> k -> a
Map.! UVar v loc
b, UVar v loc -> Set (UVar v loc)
forall a. a -> Set a
Set.singleton UVar v loc
b)
      Bool
False -> Int
-> UVar v loc
-> Map (UVar v loc) (Pretty ColorText)
-> Set (UVar v loc)
-> Solve v loc (Pretty ColorText, Set (UVar v loc))
forall v loc.
Var v =>
Int
-> UVar v loc
-> Map (UVar v loc) (Pretty ColorText)
-> Set (UVar v loc)
-> Solve v loc (Pretty ColorText, Set (UVar v loc))
prettyCyclicUVarKindWorker Int
arrPrec UVar v loc
b Map (UVar v loc) (Pretty ColorText)
nameMap Set (UVar v loc)
visitingSet
    (Pretty ColorText, Set (UVar v loc))
-> Solve v loc (Pretty ColorText, Set (UVar v loc))
forall a. a -> Solve v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Pretty ColorText -> Pretty ColorText -> Pretty ColorText
prettyArrow Int
prec Pretty ColorText
pa Pretty ColorText
pb, Set (UVar v loc)
cyclicLhs Set (UVar v loc) -> Set (UVar v loc) -> Set (UVar v loc)
forall a. Semigroup a => a -> a -> a
<> Set (UVar v loc)
cyclicRhs)

prettyCyclicUVarKindWorker ::
  (Var v) =>
  Int ->
  UVar v loc ->
  Map (UVar v loc) (P.Pretty P.ColorText) ->
  Set (UVar v loc) ->
  Solve v loc (P.Pretty P.ColorText, Set (UVar v loc))
prettyCyclicUVarKindWorker :: forall v loc.
Var v =>
Int
-> UVar v loc
-> Map (UVar v loc) (Pretty ColorText)
-> Set (UVar v loc)
-> Solve v loc (Pretty ColorText, Set (UVar v loc))
prettyCyclicUVarKindWorker Int
prec UVar v loc
u Map (UVar v loc) (Pretty ColorText)
nameMap Set (UVar v loc)
visitingSet =
  UVar v loc -> Solve v loc (Maybe (Constraint (UVar v loc) v loc))
forall v loc.
Var v =>
UVar v loc -> Solve v loc (Maybe (Constraint (UVar v loc) v loc))
find UVar v loc
u Solve v loc (Maybe (Constraint (UVar v loc) v loc))
-> (Maybe (Constraint (UVar v loc) v loc)
    -> Solve v loc (Pretty ColorText, Set (UVar v loc)))
-> Solve v loc (Pretty ColorText, Set (UVar 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
    Maybe (Constraint (UVar v loc) v loc)
Nothing -> (Pretty ColorText, Set (UVar v loc))
-> Solve v loc (Pretty ColorText, Set (UVar v loc))
forall a. a -> Solve v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Pretty ColorText
prettyUnknown Int
prec, Set (UVar v loc)
forall a. Set a
Set.empty)
    Just Constraint (UVar v loc) v loc
c -> do
      let visitingSet1 :: Set (UVar v loc)
visitingSet1 = UVar v loc -> Set (UVar v loc) -> Set (UVar v loc)
forall a. Ord a => a -> Set a -> Set a
Set.insert UVar v loc
u Set (UVar v loc)
visitingSet
      Constraint (UVar v loc) v loc
-> Int
-> Map (UVar v loc) (Pretty ColorText)
-> Set (UVar v loc)
-> Solve v loc (Pretty ColorText, Set (UVar v loc))
forall v loc.
Var v =>
Constraint (UVar v loc) v loc
-> Int
-> Map (UVar v loc) (Pretty ColorText)
-> Set (UVar v loc)
-> Solve v loc (Pretty ColorText, Set (UVar v loc))
prettyCyclicSolvedConstraint Constraint (UVar v loc) v loc
c Int
prec Map (UVar v loc) (Pretty ColorText)
nameMap Set (UVar v loc)
visitingSet1

-- | Pretty print the kind constraint on the given @UVar@.
--
-- __Precondition:__ The @ConstraintMap@ is acyclic.
tryPrettyUVarKind :: (Var v) => PrettyPrintEnv -> ConstraintMap v loc -> UVar v loc -> Either (SolveError loc) (P.Pretty P.ColorText)
tryPrettyUVarKind :: forall v loc.
Var v =>
PrettyPrintEnv
-> ConstraintMap v loc
-> UVar v loc
-> Either (SolveError loc) (Pretty ColorText)
tryPrettyUVarKind PrettyPrintEnv
ppe ConstraintMap v loc
constraints UVar v loc
uvar = PrettyPrintEnv
-> ConstraintMap v loc
-> forall r. Solve v loc r -> Either (SolveError loc) r
forall v loc.
Var v =>
PrettyPrintEnv
-> ConstraintMap v loc
-> forall r. Solve v loc r -> Either (SolveError loc) r
ppRunner PrettyPrintEnv
ppe ConstraintMap v loc
constraints do
  Int -> UVar v loc -> Solve v loc (Pretty ColorText)
forall v loc.
Var v =>
Int -> UVar v loc -> Solve v loc (Pretty ColorText)
prettyUVarKind' Int
arrPrec UVar v loc
uvar

prettyUVarKind :: (Var v) => PrettyPrintEnv -> ConstraintMap v loc -> UVar v loc -> P.Pretty P.ColorText
prettyUVarKind :: forall v loc.
Var v =>
PrettyPrintEnv
-> ConstraintMap v loc -> UVar v loc -> Pretty ColorText
prettyUVarKind PrettyPrintEnv
ppe ConstraintMap v loc
constraints UVar v loc
uvar =
  case PrettyPrintEnv
-> ConstraintMap v loc
-> UVar v loc
-> Either (SolveError loc) (Pretty ColorText)
forall v loc.
Var v =>
PrettyPrintEnv
-> ConstraintMap v loc
-> UVar v loc
-> Either (SolveError loc) (Pretty ColorText)
tryPrettyUVarKind PrettyPrintEnv
ppe ConstraintMap v loc
constraints UVar v loc
uvar of
    Left SolveError loc
solveErr -> SolveError loc -> Pretty ColorText
forall loc. SolveError loc -> Pretty ColorText
prettySolveError SolveError loc
solveErr
    Right Pretty ColorText
pp -> Pretty ColorText
pp

prettyUVarKind' :: (Var v) => Int -> UVar v loc -> Solve v loc (P.Pretty P.ColorText)
prettyUVarKind' :: forall v loc.
Var v =>
Int -> UVar v loc -> Solve v loc (Pretty ColorText)
prettyUVarKind' Int
prec UVar v loc
u =
  UVar v loc -> Solve v loc (Maybe (Constraint (UVar v loc) v loc))
forall v loc.
Var v =>
UVar v loc -> Solve v loc (Maybe (Constraint (UVar v loc) v loc))
find UVar v loc
u Solve v loc (Maybe (Constraint (UVar v loc) v loc))
-> (Maybe (Constraint (UVar v loc) v loc)
    -> Solve v loc (Pretty ColorText))
-> Solve v loc (Pretty ColorText)
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
    Maybe (Constraint (UVar v loc) v loc)
Nothing -> Pretty ColorText -> Solve v loc (Pretty ColorText)
forall a. a -> Solve v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Pretty ColorText
prettyUnknown Int
prec)
    Just Constraint (UVar v loc) v loc
c -> Int
-> Constraint (UVar v loc) v loc -> Solve v loc (Pretty ColorText)
forall v loc.
Var v =>
Int
-> Constraint (UVar v loc) v loc -> Solve v loc (Pretty ColorText)
prettySolvedConstraint' Int
prec Constraint (UVar v loc) v loc
c

-- | Pretty print a 'Solved.Constraint'
--
-- __Precondition:__ The @ConstraintMap@ is acyclic.
tryPrettySolvedConstraint ::
  (Var v) =>
  PrettyPrintEnv ->
  ConstraintMap v loc ->
  Solved.Constraint (UVar v loc) v loc ->
  Either (SolveError loc) (P.Pretty P.ColorText)
tryPrettySolvedConstraint :: forall v loc.
Var v =>
PrettyPrintEnv
-> ConstraintMap v loc
-> Constraint (UVar v loc) v loc
-> Either (SolveError loc) (Pretty ColorText)
tryPrettySolvedConstraint PrettyPrintEnv
ppe ConstraintMap v loc
constraints Constraint (UVar v loc) v loc
c =
  PrettyPrintEnv
-> ConstraintMap v loc
-> forall r. Solve v loc r -> Either (SolveError loc) r
forall v loc.
Var v =>
PrettyPrintEnv
-> ConstraintMap v loc
-> forall r. Solve v loc r -> Either (SolveError loc) r
ppRunner PrettyPrintEnv
ppe ConstraintMap v loc
constraints (Int
-> Constraint (UVar v loc) v loc -> Solve v loc (Pretty ColorText)
forall v loc.
Var v =>
Int
-> Constraint (UVar v loc) v loc -> Solve v loc (Pretty ColorText)
prettySolvedConstraint' Int
arrPrec Constraint (UVar v loc) v loc
c)

-- | Pretty print a 'Solved.Constraint'
--
-- __Precondition:__ The @ConstraintMap@ is acyclic.
prettySolvedConstraint ::
  (Var v) =>
  PrettyPrintEnv ->
  ConstraintMap v loc ->
  Solved.Constraint (UVar v loc) v loc ->
  P.Pretty P.ColorText
prettySolvedConstraint :: forall v loc.
Var v =>
PrettyPrintEnv
-> ConstraintMap v loc
-> Constraint (UVar v loc) v loc
-> Pretty ColorText
prettySolvedConstraint PrettyPrintEnv
ppe ConstraintMap v loc
constraints Constraint (UVar v loc) v loc
c =
  case PrettyPrintEnv
-> ConstraintMap v loc
-> Constraint (UVar v loc) v loc
-> Either (SolveError loc) (Pretty ColorText)
forall v loc.
Var v =>
PrettyPrintEnv
-> ConstraintMap v loc
-> Constraint (UVar v loc) v loc
-> Either (SolveError loc) (Pretty ColorText)
tryPrettySolvedConstraint PrettyPrintEnv
ppe ConstraintMap v loc
constraints Constraint (UVar v loc) v loc
c of
    Left SolveError loc
solveErr -> SolveError loc -> Pretty ColorText
forall loc. SolveError loc -> Pretty ColorText
prettySolveError SolveError loc
solveErr
    Right Pretty ColorText
pp -> Pretty ColorText
pp

prettySolvedConstraint' :: (Var v) => Int -> Solved.Constraint (UVar v loc) v loc -> Solve v loc (P.Pretty P.ColorText)
prettySolvedConstraint' :: forall v loc.
Var v =>
Int
-> Constraint (UVar v loc) v loc -> Solve v loc (Pretty ColorText)
prettySolvedConstraint' Int
prec = \case
  Solved.IsAbility Provenance v loc
_ -> Pretty ColorText -> Solve v loc (Pretty ColorText)
forall a. a -> Solve v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Pretty ColorText
prettyAbility Int
prec)
  Solved.IsType TypeProvenance v loc
_ -> Pretty ColorText -> Solve v loc (Pretty ColorText)
forall a. a -> Solve v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Pretty ColorText
prettyType Int
prec)
  Solved.IsArr Provenance v loc
_ UVar v loc
a UVar v loc
b -> do
    Pretty ColorText
a <- Int -> UVar v loc -> Solve v loc (Pretty ColorText)
forall v loc.
Var v =>
Int -> UVar v loc -> Solve v loc (Pretty ColorText)
prettyUVarKind' (Int
arrPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) UVar v loc
a
    Pretty ColorText
b <- Int -> UVar v loc -> Solve v loc (Pretty ColorText)
forall v loc.
Var v =>
Int -> UVar v loc -> Solve v loc (Pretty ColorText)
prettyUVarKind' Int
arrPrec UVar v loc
b
    pure (Int -> Pretty ColorText -> Pretty ColorText -> Pretty ColorText
prettyArrow Int
prec Pretty ColorText
a Pretty ColorText
b)

-- | Pretty printers for constraints need to look them up in the
-- constraint map, but no constraints are added. This runner just
-- allows running pretty printers outside of the @Solve@ monad by
-- discarding the resulting state.
ppRunner :: (Var v) => PrettyPrintEnv -> ConstraintMap v loc -> (forall r. Solve v loc r -> Either (SolveError loc) r)
ppRunner :: forall v loc.
Var v =>
PrettyPrintEnv
-> ConstraintMap v loc
-> forall r. Solve v loc r -> Either (SolveError loc) r
ppRunner PrettyPrintEnv
ppe ConstraintMap v loc
constraints =
  let st :: SolveState v loc
st =
        SolveState
          { $sel:unifVars:SolveState :: Set Symbol
unifVars = Set Symbol
forall a. Set a
Set.empty,
            $sel:newUnifVars:SolveState :: [UVar v loc]
newUnifVars = [],
            $sel:constraints:SolveState :: ConstraintMap v loc
constraints = ConstraintMap v loc
constraints,
            $sel:typeMap:SolveState :: Map (Type v loc) (NonEmpty (UVar v loc))
typeMap = Map (Type v loc) (NonEmpty (UVar v loc))
forall a. Monoid a => a
mempty
          }
      env :: Env
env = PrettyPrintEnv -> Env
Env PrettyPrintEnv
ppe
   in \Solve v loc r
solve -> (r, SolveState v loc) -> r
forall a b. (a, b) -> a
fst ((r, SolveState v loc) -> r)
-> Either (SolveError loc) (r, SolveState v loc)
-> Either (SolveError loc) r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Env
-> SolveState v loc
-> Solve v loc r
-> Either (SolveError loc) (r, SolveState v loc)
forall v loc a.
Env
-> SolveState v loc
-> Solve v loc a
-> Either (SolveError loc) (a, SolveState v loc)
runSolve Env
env SolveState v loc
st Solve v loc r
solve)

-- | A pretty printer for cyclic kind constraints on a
-- @UVar@. Expresses the infinite kind by a generating equation.
--
-- __Precondition:__ The @UVar@ has a cyclic constraint.
tryPrettyCyclicUVarKind ::
  (Var v) =>
  PrettyPrintEnv ->
  ConstraintMap v loc ->
  UVar v loc ->
  -- | A function to style the cyclic @UVar@'s variable name
  (P.Pretty P.ColorText -> P.Pretty P.ColorText) ->
  -- | (the pretty @UVar@ variable, the generating equation)
  Either (SolveError loc) (P.Pretty P.ColorText, P.Pretty P.ColorText)
tryPrettyCyclicUVarKind :: forall v loc.
Var v =>
PrettyPrintEnv
-> ConstraintMap v loc
-> UVar v loc
-> (Pretty ColorText -> Pretty ColorText)
-> Either (SolveError loc) (Pretty ColorText, Pretty ColorText)
tryPrettyCyclicUVarKind PrettyPrintEnv
ppe ConstraintMap v loc
constraints UVar v loc
uvar Pretty ColorText -> Pretty ColorText
theUVarStyle = PrettyPrintEnv
-> ConstraintMap v loc
-> forall r. Solve v loc r -> Either (SolveError loc) r
forall v loc.
Var v =>
PrettyPrintEnv
-> ConstraintMap v loc
-> forall r. Solve v loc r -> Either (SolveError loc) r
ppRunner PrettyPrintEnv
ppe ConstraintMap v loc
constraints do
  UVar v loc -> Solve v loc (Maybe (Constraint (UVar v loc) v loc))
forall v loc.
Var v =>
UVar v loc -> Solve v loc (Maybe (Constraint (UVar v loc) v loc))
find UVar v loc
uvar Solve v loc (Maybe (Constraint (UVar v loc) v loc))
-> (Maybe (Constraint (UVar v loc) v loc)
    -> Solve v loc (Pretty ColorText, Pretty ColorText))
-> Solve v loc (Pretty ColorText, Pretty ColorText)
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
    Maybe (Constraint (UVar v loc) v loc)
Nothing -> Solve v loc (Pretty ColorText, Pretty ColorText)
explode
    Just Constraint (UVar v loc) v loc
c -> do
      rec (Pretty ColorText
pp, Set (UVar v loc)
cyclicUVars) <- Constraint (UVar v loc) v loc
-> Int
-> Map (UVar v loc) (Pretty ColorText)
-> Set (UVar v loc)
-> Solve v loc (Pretty ColorText, Set (UVar v loc))
forall v loc.
Var v =>
Constraint (UVar v loc) v loc
-> Int
-> Map (UVar v loc) (Pretty ColorText)
-> Set (UVar v loc)
-> Solve v loc (Pretty ColorText, Set (UVar v loc))
prettyCyclicSolvedConstraint Constraint (UVar v loc) v loc
c Int
arrPrec Map (UVar v loc) (Pretty ColorText)
nameMap (UVar v loc -> Set (UVar v loc)
forall a. a -> Set a
Set.singleton UVar v loc
uvar)
          let nameMap :: Map (UVar v loc) (Pretty ColorText)
nameMap = (Int, Map (UVar v loc) (Pretty ColorText))
-> Map (UVar v loc) (Pretty ColorText)
forall a b. (a, b) -> b
snd ((Int, Map (UVar v loc) (Pretty ColorText))
 -> Map (UVar v loc) (Pretty ColorText))
-> (Int, Map (UVar v loc) (Pretty ColorText))
-> Map (UVar v loc) (Pretty ColorText)
forall a b. (a -> b) -> a -> b
$ ((Int, Map (UVar v loc) (Pretty ColorText))
 -> UVar v loc -> (Int, Map (UVar v loc) (Pretty ColorText)))
-> (Int, Map (UVar v loc) (Pretty ColorText))
-> Set (UVar v loc)
-> (Int, Map (UVar v loc) (Pretty ColorText))
forall b a. (b -> a -> b) -> b -> Set a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Int, Map (UVar v loc) (Pretty ColorText))
-> UVar v loc -> (Int, Map (UVar v loc) (Pretty ColorText))
phi (Int
0 :: Int, Map (UVar v loc) (Pretty ColorText)
forall k a. Map k a
Map.empty) Set (UVar v loc)
cyclicUVars
              phi :: (Int, Map (UVar v loc) (Pretty ColorText))
-> UVar v loc -> (Int, Map (UVar v loc) (Pretty ColorText))
phi (Int
n, Map (UVar v loc) (Pretty ColorText)
m) UVar v loc
a =
                let name :: Pretty ColorText
name = [Char] -> Pretty ColorText
forall s. IsString s => [Char] -> Pretty s
P.string (if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then [Char]
"k" else [Char]
"k" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n)
                    !newN :: Int
newN = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
                    prettyVar :: Pretty ColorText
prettyVar = case UVar v loc
a UVar v loc -> UVar v loc -> Bool
forall a. Eq a => a -> a -> Bool
== UVar v loc
uvar of
                      Bool
True -> Pretty ColorText -> Pretty ColorText
theUVarStyle Pretty ColorText
name
                      Bool
False -> Pretty ColorText
name
                    !newMap :: Map (UVar v loc) (Pretty ColorText)
newMap = UVar v loc
-> Pretty ColorText
-> Map (UVar v loc) (Pretty ColorText)
-> Map (UVar v loc) (Pretty ColorText)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert UVar v loc
a Pretty ColorText
prettyVar Map (UVar v loc) (Pretty ColorText)
m
                 in (Int
newN, Map (UVar v loc) (Pretty ColorText)
newMap)
      case UVar v loc
-> Map (UVar v loc) (Pretty ColorText) -> Maybe (Pretty ColorText)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup UVar v loc
uvar Map (UVar v loc) (Pretty ColorText)
nameMap of
        Maybe (Pretty ColorText)
Nothing -> Solve v loc (Pretty ColorText, Pretty ColorText)
explode
        Just Pretty ColorText
n -> (Pretty ColorText, Pretty ColorText)
-> Solve v loc (Pretty ColorText, Pretty ColorText)
forall a. a -> Solve v loc a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pretty ColorText
n, Pretty ColorText -> Pretty ColorText
forall s. (ListLike s Char, IsString s) => Pretty s -> Pretty s
P.wrap (Pretty ColorText
n 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
<> Pretty ColorText
pp))
  where
    explode :: Solve v loc (Pretty ColorText, Pretty ColorText)
explode = [Char] -> Solve v loc (Pretty ColorText, Pretty ColorText)
forall a. HasCallStack => [Char] -> a
error ([Char]
"[prettyCyclicUVarKind] called with non-cyclic uvar: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> UVar v loc -> [Char]
forall a. Show a => a -> [Char]
show UVar v loc
uvar)

-- | A pretty printer for cyclic kind constraints on a
-- @UVar@. Expresses the infinite kind by a generating equation.
--
-- __Precondition:__ The @UVar@ has a cyclic constraint.
prettyCyclicUVarKind ::
  (Var v) =>
  PrettyPrintEnv ->
  ConstraintMap v loc ->
  UVar v loc ->
  -- | A function to style the cyclic @UVar@'s variable name
  (P.Pretty P.ColorText -> P.Pretty P.ColorText) ->
  -- | (the pretty @UVar@ variable, the generating equation)
  (P.Pretty P.ColorText, P.Pretty P.ColorText)
prettyCyclicUVarKind :: forall v loc.
Var v =>
PrettyPrintEnv
-> ConstraintMap v loc
-> UVar v loc
-> (Pretty ColorText -> Pretty ColorText)
-> (Pretty ColorText, Pretty ColorText)
prettyCyclicUVarKind PrettyPrintEnv
ppe ConstraintMap v loc
constraints UVar v loc
uvar Pretty ColorText -> Pretty ColorText
theUVarStyle =
  case PrettyPrintEnv
-> ConstraintMap v loc
-> UVar v loc
-> (Pretty ColorText -> Pretty ColorText)
-> Either (SolveError loc) (Pretty ColorText, Pretty ColorText)
forall v loc.
Var v =>
PrettyPrintEnv
-> ConstraintMap v loc
-> UVar v loc
-> (Pretty ColorText -> Pretty ColorText)
-> Either (SolveError loc) (Pretty ColorText, Pretty ColorText)
tryPrettyCyclicUVarKind PrettyPrintEnv
ppe ConstraintMap v loc
constraints UVar v loc
uvar Pretty ColorText -> Pretty ColorText
theUVarStyle of
    Left SolveError loc
solveErr -> (SolveError loc -> Pretty ColorText
forall loc. SolveError loc -> Pretty ColorText
prettySolveError SolveError loc
solveErr, SolveError loc -> Pretty ColorText
forall loc. SolveError loc -> Pretty ColorText
prettySolveError SolveError loc
solveErr)
    Right (Pretty ColorText, Pretty ColorText)
pp -> (Pretty ColorText, Pretty ColorText)
pp

prettySolveError :: (SolveError loc) -> P.Pretty P.ColorText
prettySolveError :: forall loc. SolveError loc -> Pretty ColorText
prettySolveError = \case
  MissingBuiltin loc
_loc Reference
builtin ->
    [Pretty ColorText] -> Pretty ColorText
forall (f :: * -> *) s.
(Foldable f, IsString s) =>
f (Pretty s) -> Pretty s
P.lines
      [ Pretty ColorText
"Encountered unknown builtin when kind-checking: " Pretty ColorText -> Pretty ColorText -> Pretty ColorText
forall a. Semigroup a => a -> a -> a
<> Reference -> Pretty ColorText
forall a s. (Show a, IsString s) => a -> Pretty s
P.shown Reference
builtin,
        Pretty ColorText
"✨ Hint: Upgrading to the latest ucm may resolve this issue."
      ]