module Unison.KindInference.Error
  ( KindError (..),
    lspLoc,
    ConstraintConflict (..),
    improveError,
  )
where

import Unison.ABT qualified as ABT
import Unison.KindInference.Constraint.Context (ConstraintContext (..))
import Unison.KindInference.Constraint.Provenance (Provenance (..))
import Unison.KindInference.Constraint.Solved qualified as Solved
import Unison.KindInference.Constraint.Unsolved qualified as Unsolved
import Unison.KindInference.Generate.Monad (GeneratedConstraint)
import Unison.KindInference.Solve.Monad
  ( ConstraintMap,
    Solve (..),
  )
import Unison.KindInference.UVar (UVar (..))
import Unison.Prelude
import Unison.Type (Type)
import Unison.Var (Var)

-- | Two incompatible constraints on a @UVar@.
data ConstraintConflict v loc = ConstraintConflict'
  { forall v loc. ConstraintConflict v loc -> UVar v loc
conflictedVar :: UVar v loc,
    forall v loc.
ConstraintConflict v loc -> Constraint (UVar v loc) v loc
impliedConstraint :: Solved.Constraint (UVar v loc) v loc,
    forall v loc.
ConstraintConflict v loc -> Constraint (UVar v loc) v loc
conflictedConstraint :: Solved.Constraint (UVar v loc) v loc
  }

lspLoc :: (Semigroup loc) => KindError v loc -> loc
lspLoc :: forall loc v. Semigroup loc => KindError v loc -> loc
lspLoc = \case
  CycleDetected loc
loc UVar v loc
_ ConstraintMap v loc
_ -> loc
loc
  UnexpectedArgument loc
_ UVar v loc
abs UVar v loc
arg ConstraintMap v loc
_ -> UVar v loc -> loc
forall {v} {a}. UVar v a -> a
varLoc UVar v loc
abs loc -> loc -> loc
forall a. Semigroup a => a -> a -> a
<> UVar v loc -> loc
forall {v} {a}. UVar v a -> a
varLoc UVar v loc
arg
  ArgumentMismatch UVar v loc
abs UVar v loc
_ UVar v loc
actual ConstraintMap v loc
_ -> UVar v loc -> loc
forall {v} {a}. UVar v a -> a
varLoc UVar v loc
abs loc -> loc -> loc
forall a. Semigroup a => a -> a -> a
<> UVar v loc -> loc
forall {v} {a}. UVar v a -> a
varLoc UVar v loc
actual
  ArgumentMismatchArrow (loc, Type v loc, Type v loc)
_ ConstraintConflict' {UVar v loc
$sel:conflictedVar:ConstraintConflict' :: forall v loc. ConstraintConflict v loc -> UVar v loc
conflictedVar :: UVar v loc
conflictedVar} ConstraintMap v loc
_ -> UVar v loc -> loc
forall {v} {a}. UVar v a -> a
varLoc UVar v loc
conflictedVar
  EffectListMismatch ConstraintConflict' {UVar v loc
$sel:conflictedVar:ConstraintConflict' :: forall v loc. ConstraintConflict v loc -> UVar v loc
conflictedVar :: UVar v loc
conflictedVar} ConstraintMap v loc
_ -> UVar v loc -> loc
forall {v} {a}. UVar v a -> a
varLoc UVar v loc
conflictedVar
  ConstraintConflict GeneratedConstraint v loc
gen ConstraintConflict v loc
_ ConstraintMap v loc
_ -> GeneratedConstraint v loc
gen GeneratedConstraint v loc
-> Getting loc (GeneratedConstraint v loc) loc -> loc
forall s a. s -> Getting a s a -> a
^. Getting loc (GeneratedConstraint v loc) loc
forall uv v loc (f :: * -> *).
Functor f =>
(loc -> f loc)
-> Constraint uv v loc Provenance
-> f (Constraint uv v loc Provenance)
Unsolved.loc
  where
    varLoc :: UVar v a -> a
varLoc UVar v a
var = Term F v a -> a
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation (Term F v a -> a) -> Term F v a -> a
forall a b. (a -> b) -> a -> b
$ UVar v a -> Term F v a
forall v loc. UVar v loc -> Type v loc
uvarType UVar v a
var

-- | Errors that may arise during kind inference
data KindError v loc
  = -- | A variable is constrained to have an infinite kind
    CycleDetected loc (UVar v loc) (ConstraintMap v loc)
  | -- | Something of kind * or Effect is applied to an argument
    UnexpectedArgument
      -- | src span of abs
      loc
      -- | abs var
      (UVar v loc)
      -- | arg var
      (UVar v loc)
      -- | context
      -- | An arrow kind is applied to a type, but its kind doesn't match
      -- the expected argument kind
      (ConstraintMap v loc)
  | ArgumentMismatch
      -- | abs var
      (UVar v loc)
      -- | expected var
      (UVar v loc)
      -- | given var
      (UVar v loc)
      -- | context
      -- | Same as @ArgumentMismatch@, but for applications to the builtin
      -- @Arrow@ type.
      (ConstraintMap v loc)
  | ArgumentMismatchArrow
      -- | (The applied arrow range, lhs, rhs)
      (loc, Type v loc, Type v loc)
      (ConstraintConflict v loc)
      (ConstraintMap v loc)
  | -- | Something appeared in an effect list that isn't of kind Effect
    EffectListMismatch
      (ConstraintConflict v loc)
      (ConstraintMap v loc)
  | -- | Generic constraint conflict
    ConstraintConflict
      -- | Failed to add this constraint
      (GeneratedConstraint v loc)
      -- | Due to this conflict
      (ConstraintConflict v loc)
      -- | in this context
      (ConstraintMap v loc)

-- | Transform generic constraint conflicts into more specific error
-- by examining its @ConstraintContext@.
improveError :: (Var v) => KindError v loc -> Solve v loc (KindError v loc)
improveError :: forall v loc.
Var v =>
KindError v loc -> Solve v loc (KindError v loc)
improveError = \case
  ConstraintConflict GeneratedConstraint v loc
a ConstraintConflict v loc
b ConstraintMap v loc
c -> GeneratedConstraint v loc
-> ConstraintConflict v loc
-> ConstraintMap v loc
-> Solve v loc (KindError v loc)
forall v loc.
Var v =>
GeneratedConstraint v loc
-> ConstraintConflict v loc
-> ConstraintMap v loc
-> Solve v loc (KindError v loc)
improveError' GeneratedConstraint v loc
a ConstraintConflict v loc
b ConstraintMap v loc
c
  KindError v loc
e -> 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
e

improveError' ::
  (Var v) =>
  GeneratedConstraint v loc ->
  ConstraintConflict v loc ->
  ConstraintMap v loc ->
  Solve v loc (KindError v loc)
improveError' :: forall v loc.
Var v =>
GeneratedConstraint v loc
-> ConstraintConflict v loc
-> ConstraintMap v loc
-> Solve v loc (KindError v loc)
improveError' GeneratedConstraint v loc
generatedConstraint ConstraintConflict v loc
constraintConflict ConstraintMap v loc
constraintMap =
  let Provenance ConstraintContext v loc
ctx loc
loc = GeneratedConstraint v loc
generatedConstraint GeneratedConstraint v loc
-> Getting
     (Provenance v loc) (GeneratedConstraint v loc) (Provenance v loc)
-> Provenance v loc
forall s a. s -> Getting a s a -> a
^. Getting
  (Provenance v loc) (GeneratedConstraint v loc) (Provenance v loc)
forall uv v loc loc' (f :: * -> *).
Functor f =>
(Provenance v loc -> f (Provenance v loc'))
-> Constraint uv v loc Provenance
-> f (Constraint uv v loc' Provenance)
Unsolved.prov
   in case ConstraintContext v loc
ctx of
        AppAbs UVar v loc
abs UVar v loc
arg -> 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 (loc
-> UVar v loc
-> UVar v loc
-> ConstraintMap v loc
-> KindError v loc
forall v loc.
loc
-> UVar v loc
-> UVar v loc
-> ConstraintMap v loc
-> KindError v loc
UnexpectedArgument loc
loc UVar v loc
abs UVar v loc
arg ConstraintMap v loc
constraintMap)
        AppArg UVar v loc
abs UVar v loc
expected UVar v loc
actual -> 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 (UVar v loc
-> UVar v loc
-> UVar v loc
-> ConstraintMap v loc
-> KindError v loc
forall v loc.
UVar v loc
-> UVar v loc
-> UVar v loc
-> ConstraintMap v loc
-> KindError v loc
ArgumentMismatch UVar v loc
abs UVar v loc
expected UVar v loc
actual ConstraintMap v loc
constraintMap)
        AppArrow loc
loc Type v loc
dom Type v loc
cod -> 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 ((loc, Type v loc, Type v loc)
-> ConstraintConflict v loc
-> ConstraintMap v loc
-> KindError v loc
forall v loc.
(loc, Type v loc, Type v loc)
-> ConstraintConflict v loc
-> ConstraintMap v loc
-> KindError v loc
ArgumentMismatchArrow (loc
loc, Type v loc
dom, Type v loc
cod) ConstraintConflict v loc
constraintConflict ConstraintMap v loc
constraintMap)
        ConstraintContext v loc
EffectsList -> 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 (ConstraintConflict v loc -> ConstraintMap v loc -> KindError v loc
forall v loc.
ConstraintConflict v loc -> ConstraintMap v loc -> KindError v loc
EffectListMismatch ConstraintConflict v loc
constraintConflict ConstraintMap v loc
constraintMap)
        ConstraintContext v loc
_ -> 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 (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
generatedConstraint ConstraintConflict v loc
constraintConflict ConstraintMap v loc
constraintMap)

instance Show (KindError v loc) where
  show :: KindError v loc -> String
show KindError v loc
_ = String
"kind error"