{-# LANGUAGE BangPatterns #-}

module Unison.Typechecker.TypeError where

import Data.List.NonEmpty (NonEmpty)
import Unison.ABT qualified as ABT
import Unison.KindInference (KindError)
import Unison.Pattern (Pattern)
import Unison.Prelude hiding (whenM)
import Unison.Type (Type)
import Unison.Type qualified as Type
import Unison.Typechecker.Context qualified as C
import Unison.Typechecker.Extractor qualified as Ex
import Unison.Util.Monoid (whenM)
import Unison.Var (Var)
import Prelude hiding (all, and, or)

data BooleanMismatch = CondMismatch | AndMismatch | OrMismatch | GuardMismatch
  deriving (Int -> BooleanMismatch -> ShowS
[BooleanMismatch] -> ShowS
BooleanMismatch -> String
(Int -> BooleanMismatch -> ShowS)
-> (BooleanMismatch -> String)
-> ([BooleanMismatch] -> ShowS)
-> Show BooleanMismatch
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BooleanMismatch -> ShowS
showsPrec :: Int -> BooleanMismatch -> ShowS
$cshow :: BooleanMismatch -> String
show :: BooleanMismatch -> String
$cshowList :: [BooleanMismatch] -> ShowS
showList :: [BooleanMismatch] -> ShowS
Show)

data ExistentialMismatch = IfBody | ListBody | CaseBody
  deriving (Int -> ExistentialMismatch -> ShowS
[ExistentialMismatch] -> ShowS
ExistentialMismatch -> String
(Int -> ExistentialMismatch -> ShowS)
-> (ExistentialMismatch -> String)
-> ([ExistentialMismatch] -> ShowS)
-> Show ExistentialMismatch
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ExistentialMismatch -> ShowS
showsPrec :: Int -> ExistentialMismatch -> ShowS
$cshow :: ExistentialMismatch -> String
show :: ExistentialMismatch -> String
$cshowList :: [ExistentialMismatch] -> ShowS
showList :: [ExistentialMismatch] -> ShowS
Show)

data TypeError v loc
  = Mismatch
      { forall v loc. TypeError v loc -> Type v loc
foundType :: C.Type v loc, -- overallType1
        forall v loc. TypeError v loc -> Type v loc
expectedType :: C.Type v loc, -- overallType2
        forall v loc. TypeError v loc -> Type v loc
foundLeaf :: C.Type v loc, -- leaf1
        forall v loc. TypeError v loc -> Type v loc
expectedLeaf :: C.Type v loc, -- leaf2
        forall v loc. TypeError v loc -> Term v loc
mismatchSite :: C.Term v loc,
        forall v loc. TypeError v loc -> ErrorNote v loc
note :: C.ErrorNote v loc
      }
  | BooleanMismatch
      { forall v loc. TypeError v loc -> BooleanMismatch
getBooleanMismatch :: BooleanMismatch,
        mismatchSite :: C.Term v loc,
        foundType :: C.Type v loc,
        note :: C.ErrorNote v loc
      }
  | ExistentialMismatch
      { forall v loc. TypeError v loc -> ExistentialMismatch
getExistentialMismatch :: ExistentialMismatch,
        expectedType :: C.Type v loc,
        forall v loc. TypeError v loc -> loc
expectedLoc :: loc,
        foundType :: C.Type v loc,
        mismatchSite :: C.Term v loc,
        note :: C.ErrorNote v loc
      }
  | FunctionApplication
      { forall v loc. TypeError v loc -> Term v loc
f :: C.Term v loc,
        forall v loc. TypeError v loc -> Type v loc
ft :: C.Type v loc,
        forall v loc. TypeError v loc -> Term v loc
arg :: C.Term v loc,
        forall v loc. TypeError v loc -> Int
argNum :: Int,
        foundType :: C.Type v loc,
        expectedType :: C.Type v loc,
        forall v loc. TypeError v loc -> Maybe (Type v loc, Type v loc)
leafs :: Maybe (C.Type v loc, C.Type v loc), -- found, expected
        forall v loc. TypeError v loc -> [(v, Type v loc)]
solvedVars :: [(v, C.Type v loc)],
        note :: C.ErrorNote v loc
      }
  | NotFunctionApplication
      { f :: C.Term v loc,
        ft :: C.Type v loc,
        note :: C.ErrorNote v loc
      }
  | AbilityCheckFailure
      { forall v loc. TypeError v loc -> [Type v loc]
ambient :: [C.Type v loc],
        forall v loc. TypeError v loc -> [Type v loc]
requested :: [C.Type v loc],
        forall v loc. TypeError v loc -> loc
abilityCheckFailureSite :: loc,
        note :: C.ErrorNote v loc
      }
  | AbilityEqFailure
      { forall v loc. TypeError v loc -> [Type v loc]
lhs :: [C.Type v loc],
        forall v loc. TypeError v loc -> [Type v loc]
rhs :: [C.Type v loc],
        forall v loc. TypeError v loc -> Type v loc
tlhs :: C.Type v loc,
        forall v loc. TypeError v loc -> Type v loc
trhs :: C.Type v loc,
        abilityCheckFailureSite :: loc,
        note :: C.ErrorNote v loc
      }
  | AbilityEqFailureFromAp
      { lhs :: [C.Type v loc],
        rhs :: [C.Type v loc],
        tlhs :: C.Type v loc,
        trhs :: C.Type v loc,
        forall v loc. TypeError v loc -> Term v loc
expectedSite :: C.Term v loc,
        mismatchSite :: C.Term v loc,
        note :: C.ErrorNote v loc
      }
  | UnguardedLetRecCycle
      { forall v loc. TypeError v loc -> [v]
cycle :: [v],
        forall v loc. TypeError v loc -> [loc]
cycleLocs :: [loc],
        note :: C.ErrorNote v loc
      }
  | UnknownType
      { forall v loc. TypeError v loc -> v
unknownTypeV :: v,
        forall v loc. TypeError v loc -> loc
typeSite :: loc,
        note :: C.ErrorNote v loc
      }
  | UnknownTerm
      { forall v loc. TypeError v loc -> v
unknownTermV :: v,
        forall v loc. TypeError v loc -> loc
termSite :: loc,
        forall v loc. TypeError v loc -> [Suggestion v loc]
suggestions :: [C.Suggestion v loc],
        expectedType :: C.Type v loc,
        note :: C.ErrorNote v loc
      }
  | DuplicateDefinitions
      { forall v loc. TypeError v loc -> NonEmpty (v, [loc])
defns :: NonEmpty (v, [loc]),
        note :: C.ErrorNote v loc
      }
  | UncoveredPatterns loc (NonEmpty (Pattern ()))
  | RedundantPattern loc
  | KindInferenceFailure (KindError v loc)
  | Other (C.ErrorNote v loc)
  deriving (Int -> TypeError v loc -> ShowS
[TypeError v loc] -> ShowS
TypeError v loc -> String
(Int -> TypeError v loc -> ShowS)
-> (TypeError v loc -> String)
-> ([TypeError v loc] -> ShowS)
-> Show (TypeError v loc)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall v loc.
(Var v, Show loc, Ord loc) =>
Int -> TypeError v loc -> ShowS
forall v loc.
(Var v, Show loc, Ord loc) =>
[TypeError v loc] -> ShowS
forall v loc.
(Var v, Show loc, Ord loc) =>
TypeError v loc -> String
$cshowsPrec :: forall v loc.
(Var v, Show loc, Ord loc) =>
Int -> TypeError v loc -> ShowS
showsPrec :: Int -> TypeError v loc -> ShowS
$cshow :: forall v loc.
(Var v, Show loc, Ord loc) =>
TypeError v loc -> String
show :: TypeError v loc -> String
$cshowList :: forall v loc.
(Var v, Show loc, Ord loc) =>
[TypeError v loc] -> ShowS
showList :: [TypeError v loc] -> ShowS
Show)

type RedundantTypeAnnotation = Bool

data TypeInfo v loc = TopLevelComponent
  {forall v loc.
TypeInfo v loc -> [(v, Type v loc, RedundantTypeAnnotation)]
definitions :: [(v, Type v loc, RedundantTypeAnnotation)]}
  deriving (Int -> TypeInfo v loc -> ShowS
[TypeInfo v loc] -> ShowS
TypeInfo v loc -> String
(Int -> TypeInfo v loc -> ShowS)
-> (TypeInfo v loc -> String)
-> ([TypeInfo v loc] -> ShowS)
-> Show (TypeInfo v loc)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall v loc. Show v => Int -> TypeInfo v loc -> ShowS
forall v loc. Show v => [TypeInfo v loc] -> ShowS
forall v loc. Show v => TypeInfo v loc -> String
$cshowsPrec :: forall v loc. Show v => Int -> TypeInfo v loc -> ShowS
showsPrec :: Int -> TypeInfo v loc -> ShowS
$cshow :: forall v loc. Show v => TypeInfo v loc -> String
show :: TypeInfo v loc -> String
$cshowList :: forall v loc. Show v => [TypeInfo v loc] -> ShowS
showList :: [TypeInfo v loc] -> ShowS
Show)

type TypeNote v loc = Either (TypeError v loc) (TypeInfo v loc)

typeErrorFromNote ::
  (Ord loc, Show loc, Var v) => C.ErrorNote v loc -> TypeError v loc
typeErrorFromNote :: forall loc v.
(Ord loc, Show loc, Var v) =>
ErrorNote v loc -> TypeError v loc
typeErrorFromNote ErrorNote v loc
n = case Extractor (ErrorNote v loc) (TypeError v loc)
-> ErrorNote v loc -> Maybe (TypeError v loc)
forall e a. Extractor e a -> e -> Maybe a
Ex.extract Extractor (ErrorNote v loc) (TypeError v loc)
forall v loc.
(Var v, Ord loc) =>
ErrorExtractor v loc (TypeError v loc)
allErrors ErrorNote v loc
n of
  Just TypeError v loc
msg -> TypeError v loc
msg
  Maybe (TypeError v loc)
Nothing -> ErrorNote v loc -> TypeError v loc
forall v loc. ErrorNote v loc -> TypeError v loc
Other ErrorNote v loc
n

typeInfoFromNote ::
  (Ord loc, Show loc, Var v) => C.InfoNote v loc -> Maybe (TypeInfo v loc)
typeInfoFromNote :: forall loc v.
(Ord loc, Show loc, Var v) =>
InfoNote v loc -> Maybe (TypeInfo v loc)
typeInfoFromNote InfoNote v loc
n = case InfoNote v loc
n of
  C.TopLevelComponent [(v, Type v loc, RedundantTypeAnnotation)]
defs -> TypeInfo v loc -> Maybe (TypeInfo v loc)
forall a. a -> Maybe a
Just (TypeInfo v loc -> Maybe (TypeInfo v loc))
-> TypeInfo v loc -> Maybe (TypeInfo v loc)
forall a b. (a -> b) -> a -> b
$ [(v, Type v loc, RedundantTypeAnnotation)] -> TypeInfo v loc
forall v loc.
[(v, Type v loc, RedundantTypeAnnotation)] -> TypeInfo v loc
TopLevelComponent [(v, Type v loc, RedundantTypeAnnotation)]
defs
  InfoNote v loc
_ -> Maybe (TypeInfo v loc)
forall a. Maybe a
Nothing

allErrors ::
  (Var v, Ord loc) => Ex.ErrorExtractor v loc (TypeError v loc)
allErrors :: forall v loc.
(Var v, Ord loc) =>
ErrorExtractor v loc (TypeError v loc)
allErrors =
  [MaybeT (Reader (ErrorNote v loc)) (TypeError v loc)]
-> MaybeT (Reader (ErrorNote v loc)) (TypeError v loc)
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum
    [ MaybeT (Reader (ErrorNote v loc)) (TypeError v loc)
forall v loc.
(Var v, Ord loc) =>
ErrorExtractor v loc (TypeError v loc)
and,
      MaybeT (Reader (ErrorNote v loc)) (TypeError v loc)
forall v loc.
(Var v, Ord loc) =>
ErrorExtractor v loc (TypeError v loc)
or,
      MaybeT (Reader (ErrorNote v loc)) (TypeError v loc)
forall v loc.
(Var v, Ord loc) =>
ErrorExtractor v loc (TypeError v loc)
cond,
      MaybeT (Reader (ErrorNote v loc)) (TypeError v loc)
forall v loc.
(Var v, Ord loc) =>
ErrorExtractor v loc (TypeError v loc)
matchGuard,
      MaybeT (Reader (ErrorNote v loc)) (TypeError v loc)
forall v loc.
(Var v, Ord loc) =>
ErrorExtractor v loc (TypeError v loc)
ifBody,
      MaybeT (Reader (ErrorNote v loc)) (TypeError v loc)
forall v loc.
(Var v, Ord loc) =>
ErrorExtractor v loc (TypeError v loc)
listBody,
      MaybeT (Reader (ErrorNote v loc)) (TypeError v loc)
forall v loc.
(Var v, Ord loc) =>
ErrorExtractor v loc (TypeError v loc)
matchBody,
      MaybeT (Reader (ErrorNote v loc)) (TypeError v loc)
forall v loc. Var v => ErrorExtractor v loc (TypeError v loc)
applyingFunction,
      MaybeT (Reader (ErrorNote v loc)) (TypeError v loc)
forall v loc. Var v => ErrorExtractor v loc (TypeError v loc)
applyingNonFunction,
      MaybeT (Reader (ErrorNote v loc)) (TypeError v loc)
forall v loc.
(Var v, Ord loc) =>
ErrorExtractor v loc (TypeError v loc)
generalMismatch,
      MaybeT (Reader (ErrorNote v loc)) (TypeError v loc)
forall v a. ErrorExtractor v a (TypeError v a)
abilityCheckFailure,
      MaybeT (Reader (ErrorNote v loc)) (TypeError v loc)
forall v a. ErrorExtractor v a (TypeError v a)
abilityEqFailure,
      MaybeT (Reader (ErrorNote v loc)) (TypeError v loc)
forall v a. ErrorExtractor v a (TypeError v a)
unguardedCycle,
      MaybeT (Reader (ErrorNote v loc)) (TypeError v loc)
forall v a. ErrorExtractor v a (TypeError v a)
unknownType,
      MaybeT (Reader (ErrorNote v loc)) (TypeError v loc)
forall v loc. Var v => ErrorExtractor v loc (TypeError v loc)
unknownTerm,
      MaybeT (Reader (ErrorNote v loc)) (TypeError v loc)
forall v a. ErrorExtractor v a (TypeError v a)
duplicateDefinitions,
      MaybeT (Reader (ErrorNote v loc)) (TypeError v loc)
forall v a. ErrorExtractor v a (TypeError v a)
redundantPattern,
      MaybeT (Reader (ErrorNote v loc)) (TypeError v loc)
forall v a. ErrorExtractor v a (TypeError v a)
uncoveredPatterns,
      MaybeT (Reader (ErrorNote v loc)) (TypeError v loc)
forall v a. ErrorExtractor v a (TypeError v a)
kindInferenceFailure
    ]

topLevelComponent :: Ex.InfoExtractor v a (TypeInfo v a)
topLevelComponent :: forall v a. InfoExtractor v a (TypeInfo v a)
topLevelComponent = do
  [(v, Type v a, RedundantTypeAnnotation)]
defs <- InfoExtractor v a [(v, Type v a, RedundantTypeAnnotation)]
forall v loc.
InfoExtractor v loc [(v, Type v loc, RedundantTypeAnnotation)]
Ex.topLevelComponent
  pure $ [(v, Type v a, RedundantTypeAnnotation)] -> TypeInfo v a
forall v loc.
[(v, Type v loc, RedundantTypeAnnotation)] -> TypeInfo v loc
TopLevelComponent [(v, Type v a, RedundantTypeAnnotation)]
defs

redundantPattern :: Ex.ErrorExtractor v a (TypeError v a)
redundantPattern :: forall v a. ErrorExtractor v a (TypeError v a)
redundantPattern = do
  a
ploc <- ErrorExtractor v a a
forall v loc. ErrorExtractor v loc loc
Ex.redundantPattern
  pure (a -> TypeError v a
forall v loc. loc -> TypeError v loc
RedundantPattern a
ploc)

kindInferenceFailure :: Ex.ErrorExtractor v a (TypeError v a)
kindInferenceFailure :: forall v a. ErrorExtractor v a (TypeError v a)
kindInferenceFailure = do
  KindError v a
ke <- ErrorExtractor v a (KindError v a)
forall v loc. ErrorExtractor v loc (KindError v loc)
Ex.kindInferenceFailure
  pure (KindError v a -> TypeError v a
forall v loc. KindError v loc -> TypeError v loc
KindInferenceFailure KindError v a
ke)

uncoveredPatterns :: Ex.ErrorExtractor v a (TypeError v a)
uncoveredPatterns :: forall v a. ErrorExtractor v a (TypeError v a)
uncoveredPatterns = do
  (a
mloc, NonEmpty (Pattern ())
uncoveredCases) <- ErrorExtractor v a (a, NonEmpty (Pattern ()))
forall v loc. ErrorExtractor v loc (loc, NonEmpty (Pattern ()))
Ex.uncoveredPatterns
  TypeError v a -> ErrorExtractor v a (TypeError v a)
forall a. a -> MaybeT (Reader (ErrorNote v a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> NonEmpty (Pattern ()) -> TypeError v a
forall v loc. loc -> NonEmpty (Pattern ()) -> TypeError v loc
UncoveredPatterns a
mloc NonEmpty (Pattern ())
uncoveredCases)

abilityCheckFailure :: Ex.ErrorExtractor v a (TypeError v a)
abilityCheckFailure :: forall v a. ErrorExtractor v a (TypeError v a)
abilityCheckFailure = do
  ([Type v a]
ambient, [Type v a]
requested, Context v a
_ctx) <- ErrorExtractor v a ([Type v a], [Type v a], Context v a)
forall v loc.
ErrorExtractor v loc ([Type v loc], [Type v loc], Context v loc)
Ex.abilityCheckFailure
  Term v a
e <- ErrorExtractor v a (Term v a)
forall v loc. ErrorExtractor v loc (Term v loc)
Ex.innermostTerm
  ErrorNote v a
n <- ErrorExtractor v a (ErrorNote v a)
forall v loc. ErrorExtractor v loc (ErrorNote v loc)
Ex.errorNote
  pure $ [Type v a] -> [Type v a] -> a -> ErrorNote v a -> TypeError v a
forall v loc.
[Type v loc]
-> [Type v loc] -> loc -> ErrorNote v loc -> TypeError v loc
AbilityCheckFailure [Type v a]
ambient [Type v a]
requested (Term v a -> a
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Term v a
e) ErrorNote v a
n

abilityEqFailure :: Ex.ErrorExtractor v a (TypeError v a)
abilityEqFailure :: forall v a. ErrorExtractor v a (TypeError v a)
abilityEqFailure = do
  ([Type v a]
lhs, [Type v a]
rhs, Context v a
_ctx) <- ErrorExtractor v a ([Type v a], [Type v a], Context v a)
forall v loc.
ErrorExtractor v loc ([Type v loc], [Type v loc], Context v loc)
Ex.abilityEqFailure
  Term v a
e <- ErrorExtractor v a (Term v a)
forall v loc. ErrorExtractor v loc (Term v loc)
Ex.innermostTerm
  ErrorNote v a
n <- ErrorExtractor v a (ErrorNote v a)
forall v loc. ErrorExtractor v loc (ErrorNote v loc)
Ex.errorNote
  [PathElement v a]
path <- ErrorExtractor v a [PathElement v a]
forall v loc. ErrorExtractor v loc [PathElement v loc]
Ex.path
  (Type v a
tlhs, Type v a
trhs) : [(Type v a, Type v a)]
_ <- [(Type v a, Type v a)]
-> MaybeT (Reader (ErrorNote v a)) [(Type v a, Type v a)]
forall a. a -> MaybeT (Reader (ErrorNote v a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Type v a, Type v a)]
 -> MaybeT (Reader (ErrorNote v a)) [(Type v a, Type v a)])
-> ([PathElement v a] -> [(Type v a, Type v a)])
-> [PathElement v a]
-> MaybeT (Reader (ErrorNote v a)) [(Type v a, Type v a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PathElement v a -> Maybe (Type v a, Type v a))
-> [PathElement v a] -> [(Type v a, Type v a)]
forall a b. (a -> Maybe b) -> [a] -> [b]
forall (f :: * -> *) a b.
Filterable f =>
(a -> Maybe b) -> f a -> f b
mapMaybe PathElement v a -> Maybe (Type v a, Type v a)
forall {v} {loc}.
PathElement v loc -> Maybe (Type v loc, Type v loc)
p ([PathElement v a]
 -> MaybeT (Reader (ErrorNote v a)) [(Type v a, Type v a)])
-> [PathElement v a]
-> MaybeT (Reader (ErrorNote v a)) [(Type v a, Type v a)]
forall a b. (a -> b) -> a -> b
$ [PathElement v a] -> [PathElement v a]
forall a. [a] -> [a]
reverse [PathElement v a]
path
  let app :: ErrorExtractor v a (TypeError v a)
app = do
        ([v]
_, Term v a
f, Type v a
_, [Term v a]
_) <- SubseqExtractor v a ([v], Term v a, Type v a, [Term v a])
-> ErrorExtractor v a ([v], Term v a, Type v a, [Term v a])
forall v loc a. SubseqExtractor v loc a -> ErrorExtractor v loc a
Ex.unique SubseqExtractor v a ([v], Term v a, Type v a, [Term v a])
forall v loc.
SubseqExtractor v loc ([v], Term v loc, Type v loc, [Term v loc])
Ex.inFunctionCall
        TypeError v a -> ErrorExtractor v a (TypeError v a)
forall a. a -> MaybeT (Reader (ErrorNote v a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeError v a -> ErrorExtractor v a (TypeError v a))
-> TypeError v a -> ErrorExtractor v a (TypeError v a)
forall a b. (a -> b) -> a -> b
$ [Type v a]
-> [Type v a]
-> Type v a
-> Type v a
-> Term v a
-> Term v a
-> ErrorNote v a
-> TypeError v a
forall v loc.
[Type v loc]
-> [Type v loc]
-> Type v loc
-> Type v loc
-> Term v loc
-> Term v loc
-> ErrorNote v loc
-> TypeError v loc
AbilityEqFailureFromAp [Type v a]
lhs [Type v a]
rhs Type v a
tlhs Type v a
trhs Term v a
f Term v a
e ErrorNote v a
n
      plain :: ErrorExtractor v a (TypeError v a)
plain = TypeError v a -> ErrorExtractor v a (TypeError v a)
forall a. a -> MaybeT (Reader (ErrorNote v a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeError v a -> ErrorExtractor v a (TypeError v a))
-> TypeError v a -> ErrorExtractor v a (TypeError v a)
forall a b. (a -> b) -> a -> b
$ [Type v a]
-> [Type v a]
-> Type v a
-> Type v a
-> a
-> ErrorNote v a
-> TypeError v a
forall v loc.
[Type v loc]
-> [Type v loc]
-> Type v loc
-> Type v loc
-> loc
-> ErrorNote v loc
-> TypeError v loc
AbilityEqFailure [Type v a]
lhs [Type v a]
rhs Type v a
tlhs Type v a
trhs (Term v a -> a
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Term v a
e) ErrorNote v a
n
  ErrorExtractor v a (TypeError v a)
app ErrorExtractor v a (TypeError v a)
-> ErrorExtractor v a (TypeError v a)
-> ErrorExtractor v a (TypeError v a)
forall a.
MaybeT (Reader (ErrorNote v a)) a
-> MaybeT (Reader (ErrorNote v a)) a
-> MaybeT (Reader (ErrorNote v a)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ErrorExtractor v a (TypeError v a)
plain
  where
    p :: PathElement v loc -> Maybe (Type v loc, Type v loc)
p (C.InSubtype Type v loc
t1 Type v loc
t2) = (Type v loc, Type v loc) -> Maybe (Type v loc, Type v loc)
forall a. a -> Maybe a
Just (Type v loc
t1, Type v loc
t2)
    p (C.InEquate Type v loc
t1 Type v loc
t2) = (Type v loc, Type v loc) -> Maybe (Type v loc, Type v loc)
forall a. a -> Maybe a
Just (Type v loc
t1, Type v loc
t2)
    p PathElement v loc
_ = Maybe (Type v loc, Type v loc)
forall a. Maybe a
Nothing

duplicateDefinitions :: Ex.ErrorExtractor v a (TypeError v a)
duplicateDefinitions :: forall v a. ErrorExtractor v a (TypeError v a)
duplicateDefinitions = do
  NonEmpty (v, [a])
vs <- ErrorExtractor v a (NonEmpty (v, [a]))
forall v loc. ErrorExtractor v loc (NonEmpty (v, [loc]))
Ex.duplicateDefinitions
  ErrorNote v a
n <- ErrorExtractor v a (ErrorNote v a)
forall v loc. ErrorExtractor v loc (ErrorNote v loc)
Ex.errorNote
  pure $ NonEmpty (v, [a]) -> ErrorNote v a -> TypeError v a
forall v loc.
NonEmpty (v, [loc]) -> ErrorNote v loc -> TypeError v loc
DuplicateDefinitions NonEmpty (v, [a])
vs ErrorNote v a
n

unknownType :: Ex.ErrorExtractor v loc (TypeError v loc)
unknownType :: forall v a. ErrorExtractor v a (TypeError v a)
unknownType = do
  (loc
loc, v
v) <- ErrorExtractor v loc (loc, v)
forall v loc. ErrorExtractor v loc (loc, v)
Ex.unknownSymbol
  ErrorNote v loc
n <- ErrorExtractor v loc (ErrorNote v loc)
forall v loc. ErrorExtractor v loc (ErrorNote v loc)
Ex.errorNote
  pure $ v -> loc -> ErrorNote v loc -> TypeError v loc
forall v loc. v -> loc -> ErrorNote v loc -> TypeError v loc
UnknownType v
v loc
loc ErrorNote v loc
n

unknownTerm :: (Var v) => Ex.ErrorExtractor v loc (TypeError v loc)
unknownTerm :: forall v loc. Var v => ErrorExtractor v loc (TypeError v loc)
unknownTerm = do
  (loc
loc, v
v, [Suggestion v loc]
suggs, Type v loc
typ) <- ErrorExtractor v loc (loc, v, [Suggestion v loc], Type v loc)
forall v loc.
Var v =>
ErrorExtractor v loc (loc, v, [Suggestion v loc], Type v loc)
Ex.unknownTerm
  ErrorNote v loc
n <- ErrorExtractor v loc (ErrorNote v loc)
forall v loc. ErrorExtractor v loc (ErrorNote v loc)
Ex.errorNote
  pure $ v
-> loc
-> [Suggestion v loc]
-> Type v loc
-> ErrorNote v loc
-> TypeError v loc
forall v loc.
v
-> loc
-> [Suggestion v loc]
-> Type v loc
-> ErrorNote v loc
-> TypeError v loc
UnknownTerm v
v loc
loc [Suggestion v loc]
suggs (Type v loc -> Type v loc
forall v a. Var v => Type v a -> Type v a
Type.cleanup Type v loc
typ) ErrorNote v loc
n

generalMismatch :: (Var v, Ord loc) => Ex.ErrorExtractor v loc (TypeError v loc)
generalMismatch :: forall v loc.
(Var v, Ord loc) =>
ErrorExtractor v loc (TypeError v loc)
generalMismatch = do
  Context v loc
ctx <- ErrorExtractor v loc (Context v loc)
forall v loc. ErrorExtractor v loc (Context v loc)
Ex.typeMismatch
  let sub :: Type v loc -> Type v loc
sub Type v loc
t = Context v loc -> Type v loc -> Type v loc
forall v loc.
(Var v, Ord loc) =>
Context v loc -> Type v loc -> Type v loc
C.apply Context v loc
ctx Type v loc
t

      subtypes :: Ex.ErrorExtractor v loc [(C.Type v loc, C.Type v loc)]
      subtypes :: forall v loc. ErrorExtractor v loc [(Type v loc, Type v loc)]
subtypes = do
        [PathElement v loc]
path <- ErrorExtractor v loc [PathElement v loc]
forall v loc. ErrorExtractor v loc [PathElement v loc]
Ex.path
        pure [(Type v loc
t1, Type v loc
t2) | C.InSubtype Type v loc
t1 Type v loc
t2 <- [PathElement v loc]
path]

      firstLastSubtype ::
        Ex.ErrorExtractor
          v
          loc
          ( (C.Type v loc, C.Type v loc),
            (C.Type v loc, C.Type v loc)
          )
      firstLastSubtype :: forall v loc.
ErrorExtractor
  v loc ((Type v loc, Type v loc), (Type v loc, Type v loc))
firstLastSubtype =
        ErrorExtractor v loc [(Type v loc, Type v loc)]
forall v loc. ErrorExtractor v loc [(Type v loc, Type v loc)]
subtypes ErrorExtractor v loc [(Type v loc, Type v loc)]
-> ([(Type v loc, Type v loc)]
    -> MaybeT
         (Reader (ErrorNote v loc))
         ((Type v loc, Type v loc), (Type v loc, Type v loc)))
-> MaybeT
     (Reader (ErrorNote v loc))
     ((Type v loc, Type v loc), (Type v loc, Type v loc))
forall a b.
MaybeT (Reader (ErrorNote v loc)) a
-> (a -> MaybeT (Reader (ErrorNote v loc)) b)
-> MaybeT (Reader (ErrorNote v loc)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          [] -> MaybeT
  (Reader (ErrorNote v loc))
  ((Type v loc, Type v loc), (Type v loc, Type v loc))
forall a. MaybeT (Reader (ErrorNote v loc)) a
forall (f :: * -> *) a. Alternative f => f a
empty
          [(Type v loc, Type v loc)]
l -> ((Type v loc, Type v loc), (Type v loc, Type v loc))
-> MaybeT
     (Reader (ErrorNote v loc))
     ((Type v loc, Type v loc), (Type v loc, Type v loc))
forall a. a -> MaybeT (Reader (ErrorNote v loc)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Type v loc, Type v loc)] -> (Type v loc, Type v loc)
forall a. HasCallStack => [a] -> a
head [(Type v loc, Type v loc)]
l, [(Type v loc, Type v loc)] -> (Type v loc, Type v loc)
forall a. HasCallStack => [a] -> a
last [(Type v loc, Type v loc)]
l)
  ErrorNote v loc
n <- ErrorExtractor v loc (ErrorNote v loc)
forall v loc. ErrorExtractor v loc (ErrorNote v loc)
Ex.errorNote
  Term v loc
mismatchSite <- ErrorExtractor v loc (Term v loc)
forall v loc. ErrorExtractor v loc (Term v loc)
Ex.innermostTerm
  ((Type v loc
foundLeaf, Type v loc
expectedLeaf), (Type v loc
foundType, Type v loc
expectedType)) <- ErrorExtractor
  v loc ((Type v loc, Type v loc), (Type v loc, Type v loc))
forall v loc.
ErrorExtractor
  v loc ((Type v loc, Type v loc), (Type v loc, Type v loc))
firstLastSubtype
  case [Type v loc] -> [Type v loc]
forall v a. Var v => [Type v a] -> [Type v a]
Type.cleanups [Type v loc -> Type v loc
sub Type v loc
foundType, Type v loc -> Type v loc
sub Type v loc
expectedType, Type v loc -> Type v loc
sub Type v loc
foundLeaf, Type v loc -> Type v loc
sub Type v loc
expectedLeaf] of
    [Type v loc
ft, Type v loc
et, Type v loc
fl, Type v loc
el] -> TypeError v loc -> ErrorExtractor v loc (TypeError v loc)
forall a. a -> MaybeT (Reader (ErrorNote v loc)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeError v loc -> ErrorExtractor v loc (TypeError v loc))
-> TypeError v loc -> ErrorExtractor v loc (TypeError v loc)
forall a b. (a -> b) -> a -> b
$ Type v loc
-> Type v loc
-> Type v loc
-> Type v loc
-> Term v loc
-> ErrorNote v loc
-> TypeError v loc
forall v loc.
Type v loc
-> Type v loc
-> Type v loc
-> Type v loc
-> Term v loc
-> ErrorNote v loc
-> TypeError v loc
Mismatch Type v loc
ft Type v loc
et Type v loc
fl Type v loc
el Term v loc
mismatchSite ErrorNote v loc
n
    [Type v loc]
_ -> String -> ErrorExtractor v loc (TypeError v loc)
forall a. HasCallStack => String -> a
error String
"generalMismatch: Mismatched type binding"

and,
  or,
  cond,
  matchGuard ::
    (Var v, Ord loc) =>
    Ex.ErrorExtractor v loc (TypeError v loc)
and :: forall v loc.
(Var v, Ord loc) =>
ErrorExtractor v loc (TypeError v loc)
and = BooleanMismatch
-> SubseqExtractor v loc ()
-> ErrorExtractor v loc (TypeError v loc)
forall v loc.
(Var v, Ord loc) =>
BooleanMismatch
-> SubseqExtractor v loc ()
-> ErrorExtractor v loc (TypeError v loc)
booleanMismatch0 BooleanMismatch
AndMismatch (SubseqExtractor v loc (Type v loc, Term v loc, Int)
forall v loc. SubseqExtractor v loc (Type v loc, Term v loc, Int)
Ex.inSynthesizeApp SubseqExtractor v loc (Type v loc, Term v loc, Int)
-> SubseqExtractor v loc () -> SubseqExtractor v loc ()
forall a b.
SubseqExtractor' (ErrorNote v loc) a
-> SubseqExtractor' (ErrorNote v loc) b
-> SubseqExtractor' (ErrorNote v loc) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SubseqExtractor v loc ()
forall v loc. SubseqExtractor v loc ()
Ex.inAndApp)
or :: forall v loc.
(Var v, Ord loc) =>
ErrorExtractor v loc (TypeError v loc)
or = BooleanMismatch
-> SubseqExtractor v loc ()
-> ErrorExtractor v loc (TypeError v loc)
forall v loc.
(Var v, Ord loc) =>
BooleanMismatch
-> SubseqExtractor v loc ()
-> ErrorExtractor v loc (TypeError v loc)
booleanMismatch0 BooleanMismatch
OrMismatch (SubseqExtractor v loc (Type v loc, Term v loc, Int)
forall v loc. SubseqExtractor v loc (Type v loc, Term v loc, Int)
Ex.inSynthesizeApp SubseqExtractor v loc (Type v loc, Term v loc, Int)
-> SubseqExtractor v loc () -> SubseqExtractor v loc ()
forall a b.
SubseqExtractor' (ErrorNote v loc) a
-> SubseqExtractor' (ErrorNote v loc) b
-> SubseqExtractor' (ErrorNote v loc) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SubseqExtractor v loc ()
forall v loc. SubseqExtractor v loc ()
Ex.inOrApp)
cond :: forall v loc.
(Var v, Ord loc) =>
ErrorExtractor v loc (TypeError v loc)
cond = BooleanMismatch
-> SubseqExtractor v loc ()
-> ErrorExtractor v loc (TypeError v loc)
forall v loc.
(Var v, Ord loc) =>
BooleanMismatch
-> SubseqExtractor v loc ()
-> ErrorExtractor v loc (TypeError v loc)
booleanMismatch0 BooleanMismatch
CondMismatch SubseqExtractor v loc ()
forall v loc. SubseqExtractor v loc ()
Ex.inIfCond
matchGuard :: forall v loc.
(Var v, Ord loc) =>
ErrorExtractor v loc (TypeError v loc)
matchGuard = BooleanMismatch
-> SubseqExtractor v loc ()
-> ErrorExtractor v loc (TypeError v loc)
forall v loc.
(Var v, Ord loc) =>
BooleanMismatch
-> SubseqExtractor v loc ()
-> ErrorExtractor v loc (TypeError v loc)
booleanMismatch0 BooleanMismatch
GuardMismatch SubseqExtractor v loc ()
forall v loc. SubseqExtractor v loc ()
Ex.inMatchGuard

unguardedCycle :: Ex.ErrorExtractor v loc (TypeError v loc)
unguardedCycle :: forall v a. ErrorExtractor v a (TypeError v a)
unguardedCycle = do
  ErrorNote v loc
n <- ErrorExtractor v loc (ErrorNote v loc)
forall v loc. ErrorExtractor v loc (ErrorNote v loc)
Ex.errorNote
  C.UnguardedLetRecCycle [v]
vs [(v, Term v loc)]
es <- ErrorExtractor v loc (Cause v loc)
forall v loc. ErrorExtractor v loc (Cause v loc)
Ex.cause
  let loc :: [loc]
loc = Term v loc -> loc
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation (Term v loc -> loc)
-> ((v, Term v loc) -> Term v loc) -> (v, Term v loc) -> loc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (v, Term v loc) -> Term v loc
forall a b. (a, b) -> b
snd ((v, Term v loc) -> loc) -> [(v, Term v loc)] -> [loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(v, Term v loc)]
es
  pure $ [v] -> [loc] -> ErrorNote v loc -> TypeError v loc
forall v loc. [v] -> [loc] -> ErrorNote v loc -> TypeError v loc
UnguardedLetRecCycle [v]
vs [loc]
loc ErrorNote v loc
n

-- | helper function to support `and` / `or` / `cond`
booleanMismatch0 ::
  (Var v, Ord loc) =>
  BooleanMismatch ->
  Ex.SubseqExtractor v loc () ->
  Ex.ErrorExtractor v loc (TypeError v loc)
booleanMismatch0 :: forall v loc.
(Var v, Ord loc) =>
BooleanMismatch
-> SubseqExtractor v loc ()
-> ErrorExtractor v loc (TypeError v loc)
booleanMismatch0 BooleanMismatch
b SubseqExtractor v loc ()
ex = do
  ErrorNote v loc
n <- ErrorExtractor v loc (ErrorNote v loc)
forall v loc. ErrorExtractor v loc (ErrorNote v loc)
Ex.errorNote
  Context v loc
ctx <- ErrorExtractor v loc (Context v loc)
forall v loc. ErrorExtractor v loc (Context v loc)
Ex.typeMismatch
  let sub :: Type v loc -> Type v loc
sub Type v loc
t = Context v loc -> Type v loc -> Type v loc
forall v loc.
(Var v, Ord loc) =>
Context v loc -> Type v loc -> Type v loc
C.apply Context v loc
ctx Type v loc
t
  Term v loc
mismatchSite <- ErrorExtractor v loc (Term v loc)
forall v loc. ErrorExtractor v loc (Term v loc)
Ex.innermostTerm
  Type v loc
foundType <- SubseqExtractor v loc (Type v loc)
-> ErrorExtractor v loc (Type v loc)
forall v loc a. SubseqExtractor v loc a -> ErrorExtractor v loc a
Ex.unique (SubseqExtractor v loc (Type v loc)
 -> ErrorExtractor v loc (Type v loc))
-> SubseqExtractor v loc (Type v loc)
-> ErrorExtractor v loc (Type v loc)
forall a b. (a -> b) -> a -> b
$ do
    SubseqExtractor v loc ()
forall n. SubseqExtractor' n ()
Ex.pathStart
    (Type v loc
foundType, Type v loc
_, Maybe (Type v loc, Type v loc)
_) <- SubseqExtractor
  v loc (Type v loc, Type v loc, Maybe (Type v loc, Type v loc))
forall v loc.
SubseqExtractor
  v loc (Type v loc, Type v loc, Maybe (Type v loc, Type v loc))
inSubtypes
    SubseqExtractor' (ErrorNote v loc) [(Term v loc, Type v loc)]
-> SubseqExtractor v loc ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (SubseqExtractor' (ErrorNote v loc) [(Term v loc, Type v loc)]
 -> SubseqExtractor v loc ())
-> SubseqExtractor' (ErrorNote v loc) [(Term v loc, Type v loc)]
-> SubseqExtractor v loc ()
forall a b. (a -> b) -> a -> b
$ SubseqExtractor' (ErrorNote v loc) (Term v loc, Type v loc)
-> SubseqExtractor' (ErrorNote v loc) [(Term v loc, Type v loc)]
forall n a. SubseqExtractor' n a -> SubseqExtractor' n [a]
Ex.some SubseqExtractor' (ErrorNote v loc) (Term v loc, Type v loc)
forall v loc. SubseqExtractor v loc (Term v loc, Type v loc)
Ex.inCheck
    SubseqExtractor v loc ()
ex
    pure $ Type v loc -> Type v loc
forall v a. Var v => Type v a -> Type v a
Type.cleanup Type v loc
foundType
  pure (BooleanMismatch
-> Term v loc -> Type v loc -> ErrorNote v loc -> TypeError v loc
forall v loc.
BooleanMismatch
-> Term v loc -> Type v loc -> ErrorNote v loc -> TypeError v loc
BooleanMismatch BooleanMismatch
b Term v loc
mismatchSite (Type v loc -> Type v loc
sub Type v loc
foundType) ErrorNote v loc
n)

existentialMismatch0 ::
  (Var v, Ord loc) =>
  ExistentialMismatch ->
  Ex.SubseqExtractor v loc loc ->
  Ex.ErrorExtractor v loc (TypeError v loc)
existentialMismatch0 :: forall v loc.
(Var v, Ord loc) =>
ExistentialMismatch
-> SubseqExtractor v loc loc
-> ErrorExtractor v loc (TypeError v loc)
existentialMismatch0 ExistentialMismatch
em SubseqExtractor v loc loc
getExpectedLoc = do
  ErrorNote v loc
n <- ErrorExtractor v loc (ErrorNote v loc)
forall v loc. ErrorExtractor v loc (ErrorNote v loc)
Ex.errorNote
  Context v loc
ctx <- ErrorExtractor v loc (Context v loc)
forall v loc. ErrorExtractor v loc (Context v loc)
Ex.typeMismatch
  let sub :: Type v loc -> Type v loc
sub Type v loc
t = Context v loc -> Type v loc -> Type v loc
forall v loc.
(Var v, Ord loc) =>
Context v loc -> Type v loc -> Type v loc
C.apply Context v loc
ctx Type v loc
t
  Term v loc
mismatchSite <- ErrorExtractor v loc (Term v loc)
forall v loc. ErrorExtractor v loc (Term v loc)
Ex.innermostTerm
  ([Type v loc
foundType, Type v loc
expectedType], loc
expectedLoc) <- SubseqExtractor v loc ([Type v loc], loc)
-> ErrorExtractor v loc ([Type v loc], loc)
forall v loc a. SubseqExtractor v loc a -> ErrorExtractor v loc a
Ex.unique (SubseqExtractor v loc ([Type v loc], loc)
 -> ErrorExtractor v loc ([Type v loc], loc))
-> SubseqExtractor v loc ([Type v loc], loc)
-> ErrorExtractor v loc ([Type v loc], loc)
forall a b. (a -> b) -> a -> b
$ do
    SubseqExtractor' (ErrorNote v loc) ()
forall n. SubseqExtractor' n ()
Ex.pathStart
    subtypes :: [(Type v loc, Type v loc)]
subtypes@((Type v loc, Type v loc)
_ : [(Type v loc, Type v loc)]
_) <- SubseqExtractor' (ErrorNote v loc) (Type v loc, Type v loc)
-> SubseqExtractor' (ErrorNote v loc) [(Type v loc, Type v loc)]
forall n a. SubseqExtractor' n a -> SubseqExtractor' n [a]
Ex.some SubseqExtractor' (ErrorNote v loc) (Type v loc, Type v loc)
forall v loc. SubseqExtractor v loc (Type v loc, Type v loc)
Ex.inSubtype
    let (Type v loc
foundType, Type v loc
expectedType) = [(Type v loc, Type v loc)] -> (Type v loc, Type v loc)
forall a. HasCallStack => [a] -> a
last [(Type v loc, Type v loc)]
subtypes
    SubseqExtractor' (ErrorNote v loc) [(Term v loc, Type v loc)]
-> SubseqExtractor' (ErrorNote v loc) ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (SubseqExtractor' (ErrorNote v loc) [(Term v loc, Type v loc)]
 -> SubseqExtractor' (ErrorNote v loc) ())
-> SubseqExtractor' (ErrorNote v loc) [(Term v loc, Type v loc)]
-> SubseqExtractor' (ErrorNote v loc) ()
forall a b. (a -> b) -> a -> b
$ SubseqExtractor' (ErrorNote v loc) (Term v loc, Type v loc)
-> SubseqExtractor' (ErrorNote v loc) [(Term v loc, Type v loc)]
forall n a. SubseqExtractor' n a -> SubseqExtractor' n [a]
Ex.some SubseqExtractor' (ErrorNote v loc) (Term v loc, Type v loc)
forall v loc. SubseqExtractor v loc (Term v loc, Type v loc)
Ex.inCheck
    loc
expectedLoc <- SubseqExtractor v loc loc
getExpectedLoc
    pure ([Type v loc] -> [Type v loc]
forall v a. Var v => [Type v a] -> [Type v a]
Type.cleanups [Type v loc
foundType, Type v loc
expectedType], loc
expectedLoc)
  TypeError v loc -> ErrorExtractor v loc (TypeError v loc)
forall a. a -> MaybeT (Reader (ErrorNote v loc)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeError v loc -> ErrorExtractor v loc (TypeError v loc))
-> TypeError v loc -> ErrorExtractor v loc (TypeError v loc)
forall a b. (a -> b) -> a -> b
$
    ExistentialMismatch
-> Type v loc
-> loc
-> Type v loc
-> Term v loc
-> ErrorNote v loc
-> TypeError v loc
forall v loc.
ExistentialMismatch
-> Type v loc
-> loc
-> Type v loc
-> Term v loc
-> ErrorNote v loc
-> TypeError v loc
ExistentialMismatch
      ExistentialMismatch
em
      (Type v loc -> Type v loc
sub Type v loc
expectedType)
      loc
expectedLoc
      (Type v loc -> Type v loc
sub Type v loc
foundType)
      Term v loc
mismatchSite
      -- todo : save type leaves too
      ErrorNote v loc
n

ifBody,
  listBody,
  matchBody ::
    (Var v, Ord loc) => Ex.ErrorExtractor v loc (TypeError v loc)
ifBody :: forall v loc.
(Var v, Ord loc) =>
ErrorExtractor v loc (TypeError v loc)
ifBody = ExistentialMismatch
-> SubseqExtractor v loc loc
-> ErrorExtractor v loc (TypeError v loc)
forall v loc.
(Var v, Ord loc) =>
ExistentialMismatch
-> SubseqExtractor v loc loc
-> ErrorExtractor v loc (TypeError v loc)
existentialMismatch0 ExistentialMismatch
IfBody (SubseqExtractor v loc (Type v loc, Term v loc, Int)
forall v loc. SubseqExtractor v loc (Type v loc, Term v loc, Int)
Ex.inSynthesizeApp SubseqExtractor v loc (Type v loc, Term v loc, Int)
-> SubseqExtractor v loc loc -> SubseqExtractor v loc loc
forall a b.
SubseqExtractor' (ErrorNote v loc) a
-> SubseqExtractor' (ErrorNote v loc) b
-> SubseqExtractor' (ErrorNote v loc) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SubseqExtractor v loc loc
forall v loc. SubseqExtractor v loc loc
Ex.inIfBody)
listBody :: forall v loc.
(Var v, Ord loc) =>
ErrorExtractor v loc (TypeError v loc)
listBody = ExistentialMismatch
-> SubseqExtractor v loc loc
-> ErrorExtractor v loc (TypeError v loc)
forall v loc.
(Var v, Ord loc) =>
ExistentialMismatch
-> SubseqExtractor v loc loc
-> ErrorExtractor v loc (TypeError v loc)
existentialMismatch0 ExistentialMismatch
ListBody (SubseqExtractor v loc (Type v loc, Term v loc, Int)
forall v loc. SubseqExtractor v loc (Type v loc, Term v loc, Int)
Ex.inSynthesizeApp SubseqExtractor v loc (Type v loc, Term v loc, Int)
-> SubseqExtractor v loc loc -> SubseqExtractor v loc loc
forall a b.
SubseqExtractor' (ErrorNote v loc) a
-> SubseqExtractor' (ErrorNote v loc) b
-> SubseqExtractor' (ErrorNote v loc) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SubseqExtractor v loc loc
forall v loc. SubseqExtractor v loc loc
Ex.inVector)
matchBody :: forall v loc.
(Var v, Ord loc) =>
ErrorExtractor v loc (TypeError v loc)
matchBody = ExistentialMismatch
-> SubseqExtractor v loc loc
-> ErrorExtractor v loc (TypeError v loc)
forall v loc.
(Var v, Ord loc) =>
ExistentialMismatch
-> SubseqExtractor v loc loc
-> ErrorExtractor v loc (TypeError v loc)
existentialMismatch0 ExistentialMismatch
CaseBody (SubseqExtractor v loc ()
forall v loc. SubseqExtractor v loc ()
Ex.inMatchBody SubseqExtractor v loc ()
-> SubseqExtractor v loc loc -> SubseqExtractor v loc loc
forall a b.
SubseqExtractor' (ErrorNote v loc) a
-> SubseqExtractor' (ErrorNote v loc) b
-> SubseqExtractor' (ErrorNote v loc) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SubseqExtractor v loc loc
forall v loc. SubseqExtractor v loc loc
Ex.inMatch)

applyingNonFunction :: (Var v) => Ex.ErrorExtractor v loc (TypeError v loc)
applyingNonFunction :: forall v loc. Var v => ErrorExtractor v loc (TypeError v loc)
applyingNonFunction = do
  Context v loc
_ <- ErrorExtractor v loc (Context v loc)
forall v loc. ErrorExtractor v loc (Context v loc)
Ex.typeMismatch
  ErrorNote v loc
n <- ErrorExtractor v loc (ErrorNote v loc)
forall v loc. ErrorExtractor v loc (ErrorNote v loc)
Ex.errorNote
  (Term v loc
f, Type v loc
ft) <- SubseqExtractor' (ErrorNote v loc) (Term v loc, Type v loc)
-> ErrorExtractor v loc (Term v loc, Type v loc)
forall v loc a. SubseqExtractor v loc a -> ErrorExtractor v loc a
Ex.unique (SubseqExtractor' (ErrorNote v loc) (Term v loc, Type v loc)
 -> ErrorExtractor v loc (Term v loc, Type v loc))
-> SubseqExtractor' (ErrorNote v loc) (Term v loc, Type v loc)
-> ErrorExtractor v loc (Term v loc, Type v loc)
forall a b. (a -> b) -> a -> b
$ do
    SubseqExtractor' (ErrorNote v loc) ()
forall n. SubseqExtractor' n ()
Ex.pathStart
    (Type v loc
arity0Type, Term v loc
_arg, Int
_argNum) <- SubseqExtractor v loc (Type v loc, Term v loc, Int)
forall v loc. SubseqExtractor v loc (Type v loc, Term v loc, Int)
Ex.inSynthesizeApp
    ([v]
_, Term v loc
f, Type v loc
ft, [Term v loc]
args) <- SubseqExtractor v loc ([v], Term v loc, Type v loc, [Term v loc])
forall v loc.
SubseqExtractor v loc ([v], Term v loc, Type v loc, [Term v loc])
Ex.inFunctionCall
    let expectedArgCount :: Int
expectedArgCount = Type v loc -> Int
forall v a. Type v a -> Int
Type.arity Type v loc
ft
        foundArgCount :: Int
foundArgCount = [Term v loc] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term v loc]
args
    -- unexpectedArgLoc = ABT.annotation arg
    RedundantTypeAnnotation
-> SubseqExtractor' (ErrorNote v loc) (Term v loc, Type v loc)
-> SubseqExtractor' (ErrorNote v loc) (Term v loc, Type v loc)
forall a. Monoid a => RedundantTypeAnnotation -> a -> a
whenM (Int
expectedArgCount Int -> Int -> RedundantTypeAnnotation
forall a. Ord a => a -> a -> RedundantTypeAnnotation
< Int
foundArgCount) (SubseqExtractor' (ErrorNote v loc) (Term v loc, Type v loc)
 -> SubseqExtractor' (ErrorNote v loc) (Term v loc, Type v loc))
-> SubseqExtractor' (ErrorNote v loc) (Term v loc, Type v loc)
-> SubseqExtractor' (ErrorNote v loc) (Term v loc, Type v loc)
forall a b. (a -> b) -> a -> b
$ (Term v loc, Type v loc)
-> SubseqExtractor' (ErrorNote v loc) (Term v loc, Type v loc)
forall a. a -> SubseqExtractor' (ErrorNote v loc) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term v loc
f, Type v loc
arity0Type)
  pure $ Term v loc -> Type v loc -> ErrorNote v loc -> TypeError v loc
forall v loc.
Term v loc -> Type v loc -> ErrorNote v loc -> TypeError v loc
NotFunctionApplication Term v loc
f (Type v loc -> Type v loc
forall v a. Var v => Type v a -> Type v a
Type.cleanup Type v loc
ft) ErrorNote v loc
n

-- | Want to collect this info:
-- The `n`th argument to `f` is `foundType`, but I was expecting `expectedType`.
--
--    30 |   asdf asdf asdf
--
-- If you're curious
-- `f` has type `blah`, where
--    `a` was chosen as `A`
--    `b` was chosen as `B`
--    `c` was chosen as `C`
-- (many colors / groups)
applyingFunction :: forall v loc. (Var v) => Ex.ErrorExtractor v loc (TypeError v loc)
applyingFunction :: forall v loc. Var v => ErrorExtractor v loc (TypeError v loc)
applyingFunction = do
  ErrorNote v loc
n <- ErrorExtractor v loc (ErrorNote v loc)
forall v loc. ErrorExtractor v loc (ErrorNote v loc)
Ex.errorNote
  Context v loc
ctx <- ErrorExtractor v loc (Context v loc)
forall v loc. ErrorExtractor v loc (Context v loc)
Ex.typeMismatch
  SubseqExtractor v loc (TypeError v loc)
-> ErrorExtractor v loc (TypeError v loc)
forall v loc a. SubseqExtractor v loc a -> ErrorExtractor v loc a
Ex.unique (SubseqExtractor v loc (TypeError v loc)
 -> ErrorExtractor v loc (TypeError v loc))
-> SubseqExtractor v loc (TypeError v loc)
-> ErrorExtractor v loc (TypeError v loc)
forall a b. (a -> b) -> a -> b
$ do
    SubseqExtractor' (ErrorNote v loc) ()
forall n. SubseqExtractor' n ()
Ex.pathStart
    -- todo: make a new extrator for (some inSubtype) that pulls out the head and tail and nothing in between?
    (Type (TypeVar v loc) loc
found, Type (TypeVar v loc) loc
expected, Maybe (Type (TypeVar v loc) loc, Type (TypeVar v loc) loc)
leafs) <- SubseqExtractor
  v
  loc
  (Type (TypeVar v loc) loc, Type (TypeVar v loc) loc,
   Maybe (Type (TypeVar v loc) loc, Type (TypeVar v loc) loc))
forall v loc.
SubseqExtractor
  v loc (Type v loc, Type v loc, Maybe (Type v loc, Type v loc))
inSubtypes
    Term v loc
arg <- (Term v loc, Type (TypeVar v loc) loc) -> Term v loc
forall a b. (a, b) -> a
fst ((Term v loc, Type (TypeVar v loc) loc) -> Term v loc)
-> ([(Term v loc, Type (TypeVar v loc) loc)]
    -> (Term v loc, Type (TypeVar v loc) loc))
-> [(Term v loc, Type (TypeVar v loc) loc)]
-> Term v loc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Term v loc, Type (TypeVar v loc) loc)]
-> (Term v loc, Type (TypeVar v loc) loc)
forall a. HasCallStack => [a] -> a
head ([(Term v loc, Type (TypeVar v loc) loc)] -> Term v loc)
-> SubseqExtractor'
     (ErrorNote v loc) [(Term v loc, Type (TypeVar v loc) loc)]
-> SubseqExtractor' (ErrorNote v loc) (Term v loc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SubseqExtractor'
  (ErrorNote v loc) (Term v loc, Type (TypeVar v loc) loc)
-> SubseqExtractor'
     (ErrorNote v loc) [(Term v loc, Type (TypeVar v loc) loc)]
forall n a. SubseqExtractor' n a -> SubseqExtractor' n [a]
Ex.some SubseqExtractor'
  (ErrorNote v loc) (Term v loc, Type (TypeVar v loc) loc)
forall v loc. SubseqExtractor v loc (Term v loc, Type v loc)
Ex.inCheck
    (Type (TypeVar v loc) loc
_, Term v loc
_, Int
argIndex) <- SubseqExtractor v loc (Type (TypeVar v loc) loc, Term v loc, Int)
forall v loc. SubseqExtractor v loc (Type v loc, Term v loc, Int)
Ex.inSynthesizeApp
    ([v]
typeVars, Term v loc
f, Type (TypeVar v loc) loc
ft, [Term v loc]
_args) <- SubseqExtractor
  v loc ([v], Term v loc, Type (TypeVar v loc) loc, [Term v loc])
forall v loc.
SubseqExtractor v loc ([v], Term v loc, Type v loc, [Term v loc])
Ex.inFunctionCall
    let go :: v -> Maybe (v, C.Type v loc)
        go :: v -> Maybe (v, Type (TypeVar v loc) loc)
go v
v = (v
v,) (Type (TypeVar v loc) loc -> (v, Type (TypeVar v loc) loc))
-> (Monotype (TypeVar v loc) loc -> Type (TypeVar v loc) loc)
-> Monotype (TypeVar v loc) loc
-> (v, Type (TypeVar v loc) loc)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Monotype (TypeVar v loc) loc -> Type (TypeVar v loc) loc
forall v a. Monotype v a -> Type v a
Type.getPolytype (Monotype (TypeVar v loc) loc -> (v, Type (TypeVar v loc) loc))
-> Maybe (Monotype (TypeVar v loc) loc)
-> Maybe (v, Type (TypeVar v loc) loc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Context v loc -> v -> Maybe (Monotype (TypeVar v loc) loc)
forall v loc. Ord v => Context v loc -> v -> Maybe (Monotype v loc)
C.lookupSolved Context v loc
ctx v
v
        solvedVars :: [(v, Type (TypeVar v loc) loc)]
solvedVars = [Maybe (v, Type (TypeVar v loc) loc)]
-> [(v, Type (TypeVar v loc) loc)]
forall a. [Maybe a] -> [a]
catMaybes (v -> Maybe (v, Type (TypeVar v loc) loc)
go (v -> Maybe (v, Type (TypeVar v loc) loc))
-> [v] -> [Maybe (v, Type (TypeVar v loc) loc)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [v]
typeVars)
    let vm :: Map (TypeVar v loc) (TypeVar v loc)
vm =
          [Type (TypeVar v loc) loc] -> Map (TypeVar v loc) (TypeVar v loc)
forall v a. Var v => [Type v a] -> Map v v
Type.cleanupVarsMap ([Type (TypeVar v loc) loc] -> Map (TypeVar v loc) (TypeVar v loc))
-> [Type (TypeVar v loc) loc]
-> Map (TypeVar v loc) (TypeVar v loc)
forall a b. (a -> b) -> a -> b
$
            [Type (TypeVar v loc) loc
ft, Type (TypeVar v loc) loc
found, Type (TypeVar v loc) loc
expected]
              [Type (TypeVar v loc) loc]
-> [Type (TypeVar v loc) loc] -> [Type (TypeVar v loc) loc]
forall a. Semigroup a => a -> a -> a
<> ((Type (TypeVar v loc) loc, Type (TypeVar v loc) loc)
-> Type (TypeVar v loc) loc
forall a b. (a, b) -> a
fst ((Type (TypeVar v loc) loc, Type (TypeVar v loc) loc)
 -> Type (TypeVar v loc) loc)
-> [(Type (TypeVar v loc) loc, Type (TypeVar v loc) loc)]
-> [Type (TypeVar v loc) loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Type (TypeVar v loc) loc, Type (TypeVar v loc) loc)
-> [(Type (TypeVar v loc) loc, Type (TypeVar v loc) loc)]
forall a. Maybe a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Maybe (Type (TypeVar v loc) loc, Type (TypeVar v loc) loc)
leafs)
              [Type (TypeVar v loc) loc]
-> [Type (TypeVar v loc) loc] -> [Type (TypeVar v loc) loc]
forall a. Semigroup a => a -> a -> a
<> ((Type (TypeVar v loc) loc, Type (TypeVar v loc) loc)
-> Type (TypeVar v loc) loc
forall a b. (a, b) -> b
snd ((Type (TypeVar v loc) loc, Type (TypeVar v loc) loc)
 -> Type (TypeVar v loc) loc)
-> [(Type (TypeVar v loc) loc, Type (TypeVar v loc) loc)]
-> [Type (TypeVar v loc) loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Type (TypeVar v loc) loc, Type (TypeVar v loc) loc)
-> [(Type (TypeVar v loc) loc, Type (TypeVar v loc) loc)]
forall a. Maybe a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Maybe (Type (TypeVar v loc) loc, Type (TypeVar v loc) loc)
leafs)
              [Type (TypeVar v loc) loc]
-> [Type (TypeVar v loc) loc] -> [Type (TypeVar v loc) loc]
forall a. Semigroup a => a -> a -> a
<> ((v, Type (TypeVar v loc) loc) -> Type (TypeVar v loc) loc
forall a b. (a, b) -> b
snd ((v, Type (TypeVar v loc) loc) -> Type (TypeVar v loc) loc)
-> [(v, Type (TypeVar v loc) loc)] -> [Type (TypeVar v loc) loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(v, Type (TypeVar v loc) loc)]
solvedVars)
        cleanup :: Type (TypeVar v loc) loc -> Type (TypeVar v loc) loc
cleanup = Map (TypeVar v loc) (TypeVar v loc)
-> Type (TypeVar v loc) loc -> Type (TypeVar v loc) loc
forall v a. Var v => Map v v -> Type v a -> Type v a
Type.cleanupVars1' Map (TypeVar v loc) (TypeVar v loc)
vm (Type (TypeVar v loc) loc -> Type (TypeVar v loc) loc)
-> (Type (TypeVar v loc) loc -> Type (TypeVar v loc) loc)
-> Type (TypeVar v loc) loc
-> Type (TypeVar v loc) loc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type (TypeVar v loc) loc -> Type (TypeVar v loc) loc
forall v a. Var v => Type v a -> Type v a
Type.cleanupAbilityLists
    pure $
      Term v loc
-> Type (TypeVar v loc) loc
-> Term v loc
-> Int
-> Type (TypeVar v loc) loc
-> Type (TypeVar v loc) loc
-> Maybe (Type (TypeVar v loc) loc, Type (TypeVar v loc) loc)
-> [(v, Type (TypeVar v loc) loc)]
-> ErrorNote v loc
-> TypeError v loc
forall v loc.
Term v loc
-> Type v loc
-> Term v loc
-> Int
-> Type v loc
-> Type v loc
-> Maybe (Type v loc, Type v loc)
-> [(v, Type v loc)]
-> ErrorNote v loc
-> TypeError v loc
FunctionApplication
        Term v loc
f
        (Type (TypeVar v loc) loc -> Type (TypeVar v loc) loc
cleanup Type (TypeVar v loc) loc
ft)
        Term v loc
arg
        Int
argIndex
        (Type (TypeVar v loc) loc -> Type (TypeVar v loc) loc
cleanup Type (TypeVar v loc) loc
found)
        (Type (TypeVar v loc) loc -> Type (TypeVar v loc) loc
cleanup Type (TypeVar v loc) loc
expected)
        ((\(Type (TypeVar v loc) loc
a, Type (TypeVar v loc) loc
b) -> (Type (TypeVar v loc) loc -> Type (TypeVar v loc) loc
cleanup Type (TypeVar v loc) loc
a, Type (TypeVar v loc) loc -> Type (TypeVar v loc) loc
cleanup Type (TypeVar v loc) loc
b)) ((Type (TypeVar v loc) loc, Type (TypeVar v loc) loc)
 -> (Type (TypeVar v loc) loc, Type (TypeVar v loc) loc))
-> Maybe (Type (TypeVar v loc) loc, Type (TypeVar v loc) loc)
-> Maybe (Type (TypeVar v loc) loc, Type (TypeVar v loc) loc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Type (TypeVar v loc) loc, Type (TypeVar v loc) loc)
leafs)
        ((Type (TypeVar v loc) loc -> Type (TypeVar v loc) loc)
-> (v, Type (TypeVar v loc) loc) -> (v, Type (TypeVar v loc) loc)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Type (TypeVar v loc) loc -> Type (TypeVar v loc) loc
cleanup ((v, Type (TypeVar v loc) loc) -> (v, Type (TypeVar v loc) loc))
-> [(v, Type (TypeVar v loc) loc)]
-> [(v, Type (TypeVar v loc) loc)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(v, Type (TypeVar v loc) loc)]
solvedVars)
        ErrorNote v loc
n

inSubtypes ::
  Ex.SubseqExtractor
    v
    loc
    ( C.Type v loc,
      C.Type v loc,
      Maybe (C.Type v loc, C.Type v loc)
    )
inSubtypes :: forall v loc.
SubseqExtractor
  v loc (Type v loc, Type v loc, Maybe (Type v loc, Type v loc))
inSubtypes = do
  [(Type v loc, Type v loc)]
subtypes <- SubseqExtractor' (ErrorNote v loc) (Type v loc, Type v loc)
-> SubseqExtractor' (ErrorNote v loc) [(Type v loc, Type v loc)]
forall n a. SubseqExtractor' n a -> SubseqExtractor' n [a]
Ex.some SubseqExtractor' (ErrorNote v loc) (Type v loc, Type v loc)
forall v loc. SubseqExtractor v loc (Type v loc, Type v loc)
Ex.inSubtype
  let ((Type v loc
found, Type v loc
expected), Maybe (Type v loc, Type v loc)
leaves) = case [(Type v loc, Type v loc)]
subtypes of
        [] -> String
-> ((Type v loc, Type v loc), Maybe (Type v loc, Type v loc))
forall a. HasCallStack => String -> a
error String
"unpossible: Ex.some should only succeed on nonnull output"
        [(Type v loc
found, Type v loc
expected)] -> ((Type v loc
found, Type v loc
expected), Maybe (Type v loc, Type v loc)
forall a. Maybe a
Nothing)
        [(Type v loc, Type v loc)]
_ -> ([(Type v loc, Type v loc)] -> (Type v loc, Type v loc)
forall a. HasCallStack => [a] -> a
last [(Type v loc, Type v loc)]
subtypes, (Type v loc, Type v loc) -> Maybe (Type v loc, Type v loc)
forall a. a -> Maybe a
Just ((Type v loc, Type v loc) -> Maybe (Type v loc, Type v loc))
-> (Type v loc, Type v loc) -> Maybe (Type v loc, Type v loc)
forall a b. (a -> b) -> a -> b
$ [(Type v loc, Type v loc)] -> (Type v loc, Type v loc)
forall a. HasCallStack => [a] -> a
head [(Type v loc, Type v loc)]
subtypes)
  (Type v loc, Type v loc, Maybe (Type v loc, Type v loc))
-> SubseqExtractor
     v loc (Type v loc, Type v loc, Maybe (Type v loc, Type v loc))
forall a. a -> SubseqExtractor' (ErrorNote v loc) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type v loc
found, Type v loc
expected, Maybe (Type v loc, Type v loc)
leaves)