{-# 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 qualified as Typechecker
import Unison.Typechecker.Context qualified as C
import Unison.Typechecker.Extractor qualified as Ex
import Unison.Typechecker.TypeVar (lowerType)
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)

-- | Additional mismatch info, which can be useful for providing hints in error messages.
data MismatchInfo
  = MissingDelay
  | SuperfluousDelay
  deriving (Int -> MismatchInfo -> ShowS
[MismatchInfo] -> ShowS
MismatchInfo -> String
(Int -> MismatchInfo -> ShowS)
-> (MismatchInfo -> String)
-> ([MismatchInfo] -> ShowS)
-> Show MismatchInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MismatchInfo -> ShowS
showsPrec :: Int -> MismatchInfo -> ShowS
$cshow :: MismatchInfo -> String
show :: MismatchInfo -> String
$cshowList :: [MismatchInfo] -> ShowS
showList :: [MismatchInfo] -> ShowS
Show, MismatchInfo -> MismatchInfo -> Bool
(MismatchInfo -> MismatchInfo -> Bool)
-> (MismatchInfo -> MismatchInfo -> Bool) -> Eq MismatchInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MismatchInfo -> MismatchInfo -> Bool
== :: MismatchInfo -> MismatchInfo -> Bool
$c/= :: MismatchInfo -> MismatchInfo -> Bool
/= :: MismatchInfo -> MismatchInfo -> Bool
Eq, Eq MismatchInfo
Eq MismatchInfo =>
(MismatchInfo -> MismatchInfo -> Ordering)
-> (MismatchInfo -> MismatchInfo -> Bool)
-> (MismatchInfo -> MismatchInfo -> Bool)
-> (MismatchInfo -> MismatchInfo -> Bool)
-> (MismatchInfo -> MismatchInfo -> Bool)
-> (MismatchInfo -> MismatchInfo -> MismatchInfo)
-> (MismatchInfo -> MismatchInfo -> MismatchInfo)
-> Ord MismatchInfo
MismatchInfo -> MismatchInfo -> Bool
MismatchInfo -> MismatchInfo -> Ordering
MismatchInfo -> MismatchInfo -> MismatchInfo
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: MismatchInfo -> MismatchInfo -> Ordering
compare :: MismatchInfo -> MismatchInfo -> Ordering
$c< :: MismatchInfo -> MismatchInfo -> Bool
< :: MismatchInfo -> MismatchInfo -> Bool
$c<= :: MismatchInfo -> MismatchInfo -> Bool
<= :: MismatchInfo -> MismatchInfo -> Bool
$c> :: MismatchInfo -> MismatchInfo -> Bool
> :: MismatchInfo -> MismatchInfo -> Bool
$c>= :: MismatchInfo -> MismatchInfo -> Bool
>= :: MismatchInfo -> MismatchInfo -> Bool
$cmax :: MismatchInfo -> MismatchInfo -> MismatchInfo
max :: MismatchInfo -> MismatchInfo -> MismatchInfo
$cmin :: MismatchInfo -> MismatchInfo -> MismatchInfo
min :: MismatchInfo -> MismatchInfo -> MismatchInfo
Ord)

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,
        forall v loc. TypeError v loc -> Maybe MismatchInfo
additionalInfo :: Maybe MismatchInfo
      }
  | 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
      }
  | ActionRestrictionFailure
      { 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,
        forall v loc. TypeError v loc -> [Term v loc]
args :: [C.Term v loc]
      }
  | FunctionUnderApplied
      { foundType :: C.Type v loc, -- overallType1
        expectedType :: C.Type v loc, -- overallType2
        foundLeaf :: C.Type v loc, -- leaf1
        expectedLeaf :: C.Type v loc, -- leaf2
        mismatchSite :: C.Term v loc,
        note :: C.ErrorNote v loc,
        forall v loc. TypeError v loc -> [Type v loc]
needArgs :: [Type 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
      }
  | AbilitySubtypeFailure
      { forall v loc. TypeError v loc -> [Type v loc]
sub :: [C.Type v loc],
        forall v loc. TypeError v loc -> [Type v loc]
sup :: [C.Type v loc],
        forall v loc. TypeError v loc -> Type v loc
tsub :: C.Type v loc,
        forall v loc. TypeError v loc -> Type v loc
tsup :: C.Type v 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
      }
  | AbilityInstantiationFailure
      { forall v loc. TypeError v loc -> v
var :: v,
        forall v loc. TypeError v loc -> [Type v loc]
inst :: [C.Type v loc],
        forall v loc. TypeError v loc -> Term v loc
instSite :: 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, Bool)]
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, Bool)]
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, Bool)] -> TypeInfo v loc
forall v loc. [(v, Type v loc, Bool)] -> TypeInfo v loc
TopLevelComponent [(v, Type v loc, Bool)]
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)
actionRestriction,
      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)
abilitySubFailure,
      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)
abilityCheckFailure,
      MaybeT (Reader (ErrorNote v loc)) (TypeError v loc)
forall v loc.
(Var v, Ord loc) =>
ErrorExtractor v loc (TypeError v loc)
badEffectInstantiation,
      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, Bool)]
defs <- InfoExtractor v a [(v, Type v a, Bool)]
forall v loc. InfoExtractor v loc [(v, Type v loc, Bool)]
Ex.topLevelComponent
  pure $ [(v, Type v a, Bool)] -> TypeInfo v a
forall v loc. [(v, Type v loc, Bool)] -> TypeInfo v loc
TopLevelComponent [(v, Type v a, Bool)]
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

abilitySubFailure :: Ex.ErrorExtractor v a (TypeError v a)
abilitySubFailure :: forall v a. ErrorExtractor v a (TypeError v a)
abilitySubFailure = do
  ([Type v a]
sup, [Type v a]
sub, 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
  a
failSite <- Term (F (TypeVar v a) a a) v a -> a
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation (Term (F (TypeVar v a) a a) v a -> a)
-> MaybeT (Reader (ErrorNote v a)) (Term (F (TypeVar v a) a a) v a)
-> MaybeT (Reader (ErrorNote v a)) a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MaybeT (Reader (ErrorNote v a)) (Term (F (TypeVar v a) a a) v a)
forall v loc. ErrorExtractor v loc (Term v loc)
Ex.innermostTerm
  ErrorNote v a
note <- 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
tsub, Type v a
tsup) : [(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
  pure $ [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
AbilitySubtypeFailure [Type v a]
sub [Type v a]
sup Type v a
tsub Type v a
tsup a
failSite ErrorNote v a
note
  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 PathElement v loc
_ = Maybe (Type v loc, Type v loc)
forall a. Maybe a
Nothing

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, NESet a)
vs <- ErrorExtractor v a (NonEmpty (v, NESet a))
forall v loc. ErrorExtractor v loc (NonEmpty (v, NESet 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, NESet a)
vs NonEmpty (v, NESet a)
-> ((v, NESet a) -> (v, [a])) -> NonEmpty (v, [a])
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (NESet a -> [a]) -> (v, NESet a) -> (v, [a])
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 NESet a -> [a]
forall a. NESet a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList) 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

data EffInst v loc
  = Eff [C.Type v loc] [C.Type v loc] -- want, have
  | Normal

-- checks if the top of the path was an instantiation, and indicates
-- whether it was from an ability variable.
instantiation ::
  (Var v, Ord loc) =>
  Ex.ErrorExtractor v loc (v, C.Type v loc, EffInst v loc)
instantiation :: forall v loc.
(Var v, Ord loc) =>
ErrorExtractor v loc (v, Type v loc, EffInst v loc)
instantiation =
  ErrorExtractor v loc [PathElement v loc]
forall v loc. ErrorExtractor v loc [PathElement v loc]
Ex.path ErrorExtractor v loc [PathElement v loc]
-> ([PathElement v loc]
    -> MaybeT
         (Reader (ErrorNote v loc)) (v, Type v loc, EffInst v loc))
-> MaybeT (Reader (ErrorNote v loc)) (v, Type v loc, EffInst 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
    C.InInstantiateR Type v loc
ty v
v : [PathElement v loc]
path -> (v, Type v loc, EffInst v loc)
-> MaybeT (Reader (ErrorNote v loc)) (v, Type v loc, EffInst v loc)
forall a. a -> MaybeT (Reader (ErrorNote v loc)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((v, Type v loc, EffInst v loc)
 -> MaybeT
      (Reader (ErrorNote v loc)) (v, Type v loc, EffInst v loc))
-> (v, Type v loc, EffInst v loc)
-> MaybeT (Reader (ErrorNote v loc)) (v, Type v loc, EffInst v loc)
forall a b. (a -> b) -> a -> b
$ v
-> Type v loc
-> [PathElement v loc]
-> (v, Type v loc, EffInst v loc)
forall {a} {b} {v} {loc}.
a -> b -> [PathElement v loc] -> (a, b, EffInst v loc)
classify v
v Type v loc
ty [PathElement v loc]
path
    C.InInstantiateL v
v Type v loc
ty : [PathElement v loc]
path -> (v, Type v loc, EffInst v loc)
-> MaybeT (Reader (ErrorNote v loc)) (v, Type v loc, EffInst v loc)
forall a. a -> MaybeT (Reader (ErrorNote v loc)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((v, Type v loc, EffInst v loc)
 -> MaybeT
      (Reader (ErrorNote v loc)) (v, Type v loc, EffInst v loc))
-> (v, Type v loc, EffInst v loc)
-> MaybeT (Reader (ErrorNote v loc)) (v, Type v loc, EffInst v loc)
forall a b. (a -> b) -> a -> b
$ v
-> Type v loc
-> [PathElement v loc]
-> (v, Type v loc, EffInst v loc)
forall {a} {b} {v} {loc}.
a -> b -> [PathElement v loc] -> (a, b, EffInst v loc)
classify v
v Type v loc
ty [PathElement v loc]
path
    [PathElement v loc]
_ -> MaybeT (Reader (ErrorNote v loc)) (v, Type v loc, EffInst v loc)
forall a. MaybeT (Reader (ErrorNote v loc)) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  where
    classify :: a -> b -> [PathElement v loc] -> (a, b, EffInst v loc)
classify a
v b
ty (C.InSubAbilities [Type v loc]
want [Type v loc]
have : [PathElement v loc]
_) =
      (a
v, b
ty, [Type v loc] -> [Type v loc] -> EffInst v loc
forall v loc. [Type v loc] -> [Type v loc] -> EffInst v loc
Eff [Type v loc]
want [Type v loc]
have)
    classify a
v b
ty [PathElement v loc]
_ = (a
v, b
ty, EffInst v loc
forall v loc. EffInst v loc
Normal)

badEffectInstantiation ::
  (Var v, Ord loc) => Ex.ErrorExtractor v loc (TypeError v loc)
badEffectInstantiation :: forall v loc.
(Var v, Ord loc) =>
ErrorExtractor v loc (TypeError v loc)
badEffectInstantiation = 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
  (v
v, Type v loc
_ty, EffInst v loc
isEff) <- ErrorExtractor v loc (v, Type v loc, EffInst v loc)
forall v loc.
(Var v, Ord loc) =>
ErrorExtractor v loc (v, Type v loc, EffInst v loc)
instantiation
  Eff [Type v loc]
want [Type v loc]
_ <- EffInst v loc -> MaybeT (Reader (ErrorNote v loc)) (EffInst v loc)
forall a. a -> MaybeT (Reader (ErrorNote v loc)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure EffInst v loc
isEff
  ErrorNote v loc
n <- ErrorExtractor v loc (ErrorNote v loc)
forall v loc. ErrorExtractor v loc (ErrorNote v loc)
Ex.errorNote
  Term v loc
site <- ErrorExtractor v loc (Term v loc)
forall v loc. ErrorExtractor v loc (Term v loc)
Ex.innermostTerm
  pure $
    v
-> [Type v loc] -> Term v loc -> ErrorNote v loc -> TypeError v loc
forall v loc.
v
-> [Type v loc] -> Term v loc -> ErrorNote v loc -> TypeError v loc
AbilityInstantiationFailure v
v ([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]) -> [Type v loc] -> [Type v loc]
forall a b. (a -> b) -> a -> b
$ Type v loc -> Type v loc
sub (Type v loc -> Type v loc) -> [Type v loc] -> [Type v loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type v loc]
want) Term v loc
site 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
  let mayNeedArgs :: Maybe [Type v loc]
mayNeedArgs = Type v loc -> Type v loc -> Maybe [Type v loc]
forall {v} {a}.
(Var v, Ord a) =>
Term F (TypeVar v a) a
-> Term F (TypeVar v a) a -> Maybe [Term F (TypeVar v a) a]
findUnderApplication Type v loc
foundLeaf Type v loc
expectedLeaf
  -- If the found type is a function, and the result of that function matches the expected type,
  -- it's likely we're missing some arguments from a function.

  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] -> do
      let delayMismatch :: Maybe (Either (Type v loc) (Type v loc))
delayMismatch = Type v loc
-> Type v loc -> Maybe (Either (Type v loc) (Type v loc))
forall v loc.
Var v =>
Type v loc
-> Type v loc -> Maybe (Either (Type v loc) (Type v loc))
Typechecker.isMismatchMissingDelay Type v loc
foundType Type v loc
expectedType
      case (Maybe [Type v loc]
mayNeedArgs, Maybe (Either (Type v loc) (Type v loc))
delayMismatch) of
        (Maybe [Type v loc]
_, Just (Left {})) -> 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
-> Maybe MismatchInfo
-> TypeError v loc
forall v loc.
Type v loc
-> Type v loc
-> Type v loc
-> Type v loc
-> Term v loc
-> ErrorNote v loc
-> Maybe MismatchInfo
-> 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 (MismatchInfo -> Maybe MismatchInfo
forall a. a -> Maybe a
Just MismatchInfo
MissingDelay)
        (Maybe [Type v loc]
_, Just (Right {})) -> 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
-> Maybe MismatchInfo
-> TypeError v loc
forall v loc.
Type v loc
-> Type v loc
-> Type v loc
-> Type v loc
-> Term v loc
-> ErrorNote v loc
-> Maybe MismatchInfo
-> 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 (MismatchInfo -> Maybe MismatchInfo
forall a. a -> Maybe a
Just MismatchInfo
SuperfluousDelay)
        (Just [Type v loc]
needArgs, Maybe (Either (Type v loc) (Type v loc))
_) -> 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
-> [Type 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
-> [Type v loc]
-> TypeError v loc
FunctionUnderApplied 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 -> Type v loc
forall v b a. Ord v => Type (TypeVar b v) a -> Type v a
lowerType (Type v loc -> Type v loc) -> [Type v loc] -> [Type v loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type v loc]
needArgs)
        (Maybe [Type v loc], Maybe (Either (Type v loc) (Type v loc)))
_ -> do
          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
-> Maybe MismatchInfo
-> TypeError v loc
forall v loc.
Type v loc
-> Type v loc
-> Type v loc
-> Type v loc
-> Term v loc
-> ErrorNote v loc
-> Maybe MismatchInfo
-> 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 Maybe MismatchInfo
forall a. Maybe a
Nothing
    [Type v loc]
_ -> String -> ErrorExtractor v loc (TypeError v loc)
forall a. HasCallStack => String -> a
error String
"generalMismatch: Mismatched type binding"
  where
    findUnderApplication :: Term F (TypeVar v a) a
-> Term F (TypeVar v a) a -> Maybe [Term F (TypeVar v a) a]
findUnderApplication Term F (TypeVar v a) a
found Term F (TypeVar v a) a
expected
      | Right Bool
True <- Term F (TypeVar v a) a
-> Term F (TypeVar v a) a -> Either (CompilerBug v a) Bool
forall v loc.
(Var v, Ord loc) =>
Type v loc -> Type v loc -> Either (CompilerBug v loc) Bool
C.isSubtype Term F (TypeVar v a) a
found Term F (TypeVar v a) a
expected = [Term F (TypeVar v a) a] -> Maybe [Term F (TypeVar v a) a]
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
      | Bool
otherwise =
          case Term F (TypeVar v a) a
found of
            Type.Arrow' Term F (TypeVar v a) a
i Term F (TypeVar v a) a
o -> (Term F (TypeVar v a) a
i Term F (TypeVar v a) a
-> [Term F (TypeVar v a) a] -> [Term F (TypeVar v a) a]
forall a. a -> [a] -> [a]
:) ([Term F (TypeVar v a) a] -> [Term F (TypeVar v a) a])
-> Maybe [Term F (TypeVar v a) a] -> Maybe [Term F (TypeVar v a) a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term F (TypeVar v a) a
-> Term F (TypeVar v a) a -> Maybe [Term F (TypeVar v a) a]
findUnderApplication Term F (TypeVar v a) a
o Term F (TypeVar v a) a
expected
            Type.ForallNamed' TypeVar v a
_ Term F (TypeVar v a) a
body -> Term F (TypeVar v a) a
-> Term F (TypeVar v a) a -> Maybe [Term F (TypeVar v a) a]
findUnderApplication Term F (TypeVar v a) a
body Term F (TypeVar v a) a
expected
            Type.Effect' [Term F (TypeVar v a) a]
_ Term F (TypeVar v a) a
inner -> Term F (TypeVar v a) a
-> Term F (TypeVar v a) a -> Maybe [Term F (TypeVar v a) a]
findUnderApplication Term F (TypeVar v a) a
inner Term F (TypeVar v a) a
expected
            Term F (TypeVar v a) a
_ -> Maybe [Term F (TypeVar v a) a]
forall a. Maybe a
Nothing

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

actionRestriction ::
  (Var v, Ord loc) =>
  Ex.ErrorExtractor v loc (TypeError v loc)
actionRestriction :: forall v loc.
(Var v, Ord loc) =>
ErrorExtractor v loc (TypeError v loc)
actionRestriction = do
  SubseqExtractor v loc () -> ErrorExtractor v loc ()
forall v loc a. SubseqExtractor v loc a -> ErrorExtractor v loc a
Ex.unique SubseqExtractor v loc ()
forall v loc. SubseqExtractor v loc ()
Ex.inActionRestriction
  ErrorNote v loc
note <- 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
  [PathElement v loc]
path <- ErrorExtractor v loc [PathElement v loc]
forall v loc. ErrorExtractor v loc [PathElement v loc]
Ex.path
  let subtypes :: [Type v loc]
subtypes = [Type v loc
t1 | C.InSubtype Type v loc
t1 Type v loc
_ <- [PathElement v loc]
path]
  Bool -> ErrorExtractor v loc ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> ErrorExtractor v loc ())
-> (Bool -> Bool) -> Bool -> ErrorExtractor v loc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not (Bool -> ErrorExtractor v loc ())
-> Bool -> ErrorExtractor v loc ()
forall a b. (a -> b) -> a -> b
$ [Type v loc] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type v loc]
subtypes
  let foundType :: Type v loc
foundType = Type v loc -> Type v loc
forall v a. Var v => Type v a -> Type v a
Type.cleanup (Type v loc -> Type v loc) -> Type v loc -> Type v loc
forall a b. (a -> b) -> a -> b
$ [Type v loc] -> Type v loc
forall a. HasCallStack => [a] -> a
last [Type v loc]
subtypes
  pure $ Type v loc -> Term v loc -> ErrorNote v loc -> TypeError v loc
forall v loc.
Type v loc -> Term v loc -> ErrorNote v loc -> TypeError v loc
ActionRestrictionFailure Type v loc
foundType Term v loc
mismatchSite ErrorNote v loc
note

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, [Term v loc]
args) <- SubseqExtractor'
  (ErrorNote v loc) (Term v loc, Type v loc, [Term v loc])
-> ErrorExtractor v loc (Term v loc, Type v loc, [Term 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, [Term v loc])
 -> ErrorExtractor v loc (Term v loc, Type v loc, [Term v loc]))
-> SubseqExtractor'
     (ErrorNote v loc) (Term v loc, Type v loc, [Term v loc])
-> ErrorExtractor v loc (Term v loc, Type v loc, [Term v loc])
forall a b. (a -> b) -> a -> b
$ do
    SubseqExtractor' (ErrorNote v loc) ()
forall n. SubseqExtractor' n ()
Ex.pathStart
    (Type v loc, Term v loc, Int)
_synthApp <- 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.arityIgnoringEffects 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
    Bool
-> SubseqExtractor'
     (ErrorNote v loc) (Term v loc, Type v loc, [Term v loc])
-> SubseqExtractor'
     (ErrorNote v loc) (Term v loc, Type v loc, [Term v loc])
forall a. Monoid a => Bool -> a -> a
whenM (Int
expectedArgCount Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
foundArgCount) (SubseqExtractor'
   (ErrorNote v loc) (Term v loc, Type v loc, [Term v loc])
 -> SubseqExtractor'
      (ErrorNote v loc) (Term v loc, Type v loc, [Term v loc]))
-> SubseqExtractor'
     (ErrorNote v loc) (Term v loc, Type v loc, [Term v loc])
-> SubseqExtractor'
     (ErrorNote v loc) (Term v loc, Type v loc, [Term v loc])
forall a b. (a -> b) -> a -> b
$ (Term v loc, Type v loc, [Term v loc])
-> SubseqExtractor'
     (ErrorNote v loc) (Term v loc, Type v loc, [Term 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
ft, [Term v loc]
args)
  pure $ Term v loc
-> Type v loc -> ErrorNote v loc -> [Term v loc] -> TypeError v loc
forall v loc.
Term v loc
-> Type v loc -> ErrorNote v loc -> [Term 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 [Term v loc]
args

-- | 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)