{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}

module Inferno.Infer.Error where

import Data.Functor.Foldable (cata, embed)
import Data.Functor.Foldable.TH (makeBaseFunctor)
import qualified Data.Set as Set
import Inferno.Infer.Env (Namespace)
import Inferno.Infer.Exhaustiveness (Pattern)
import Inferno.Types.Syntax
  ( ExtIdent,
    Ident,
    ModuleName,
    Pat,
    Scoped,
  )
import Inferno.Types.Type
  ( InfernoType,
    Substitutable (..),
    TV,
    TypeClass,
  )
import Inferno.Types.VersionControl (Pinned, VCObjectHash)

type Location a = (a, a)

data TypeError a
  = UnificationFail (Set.Set TypeClass) InfernoType InfernoType (Location a)
  | ExpectedFunction (Set.Set TypeClass) InfernoType InfernoType (Location a)
  | InfiniteType TV InfernoType (Location a)
  | UnboundNameInNamespace (Scoped ModuleName) (Either VCObjectHash Namespace) (Location a)
  | UnboundExtIdent (Scoped ModuleName) ExtIdent (Location a)
  | -- | UnificationMismatch (Set.Set TypeClass) InfernoType InfernoType (Location a)
    -- | Ambiguous [Constraint]
    ImplicitVarTypeOverlap (Set.Set TypeClass) ExtIdent InfernoType InfernoType (Location a)
  | VarMultipleOccurrence Ident (Location a) (Location a)
  | IfConditionMustBeBool (Set.Set TypeClass) InfernoType (Location a)
  | AssertConditionMustBeBool (Set.Set TypeClass) InfernoType (Location a)
  | IfBranchesMustBeEqType (Set.Set TypeClass) InfernoType InfernoType (Location a) (Location a)
  | CaseBranchesMustBeEqType (Set.Set TypeClass) InfernoType InfernoType (Location a) (Location a)
  | PatternUnificationFail InfernoType InfernoType (Pat (Pinned VCObjectHash) a) (Location a)
  | PatternsMustBeEqType (Set.Set TypeClass) InfernoType InfernoType (Pat (Pinned VCObjectHash) a) (Pat (Pinned VCObjectHash) a) (Location a) (Location a)
  | -- | TypeClassUnificationError InfernoType InfernoType TypeClass (Location a)
    TypeClassNotFoundError (Set.Set TypeClass) TypeClass (Location a)
  | TypeClassNoPartialMatch TypeClass (Location a)
  | CouldNotFindTypeclassWitness (Set.Set TypeClass) (Location a)
  | NonExhaustivePatternMatch Pattern (Location a)
  | UselessPattern (Maybe (Pat (Pinned VCObjectHash) a)) (Location a)
  | ModuleNameTaken ModuleName (Location a)
  | ModuleDoesNotExist ModuleName (Location a)
  | NameInModuleDoesNotExist ModuleName Ident (Location a)
  | AmbiguousName ModuleName Namespace (Location a)
  deriving (Int -> TypeError a -> ShowS
forall a. Show a => Int -> TypeError a -> ShowS
forall a. Show a => [TypeError a] -> ShowS
forall a. Show a => TypeError a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeError a] -> ShowS
$cshowList :: forall a. Show a => [TypeError a] -> ShowS
show :: TypeError a -> String
$cshow :: forall a. Show a => TypeError a -> String
showsPrec :: Int -> TypeError a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> TypeError a -> ShowS
Show, TypeError a -> TypeError a -> Bool
forall a. Eq a => TypeError a -> TypeError a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypeError a -> TypeError a -> Bool
$c/= :: forall a. Eq a => TypeError a -> TypeError a -> Bool
== :: TypeError a -> TypeError a -> Bool
$c== :: forall a. Eq a => TypeError a -> TypeError a -> Bool
Eq, TypeError a -> TypeError a -> Ordering
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
forall {a}. Ord a => Eq (TypeError a)
forall a. Ord a => TypeError a -> TypeError a -> Bool
forall a. Ord a => TypeError a -> TypeError a -> Ordering
forall a. Ord a => TypeError a -> TypeError a -> TypeError a
min :: TypeError a -> TypeError a -> TypeError a
$cmin :: forall a. Ord a => TypeError a -> TypeError a -> TypeError a
max :: TypeError a -> TypeError a -> TypeError a
$cmax :: forall a. Ord a => TypeError a -> TypeError a -> TypeError a
>= :: TypeError a -> TypeError a -> Bool
$c>= :: forall a. Ord a => TypeError a -> TypeError a -> Bool
> :: TypeError a -> TypeError a -> Bool
$c> :: forall a. Ord a => TypeError a -> TypeError a -> Bool
<= :: TypeError a -> TypeError a -> Bool
$c<= :: forall a. Ord a => TypeError a -> TypeError a -> Bool
< :: TypeError a -> TypeError a -> Bool
$c< :: forall a. Ord a => TypeError a -> TypeError a -> Bool
compare :: TypeError a -> TypeError a -> Ordering
$ccompare :: forall a. Ord a => TypeError a -> TypeError a -> Ordering
Ord, forall a. Eq a => a -> TypeError a -> Bool
forall a. Num a => TypeError a -> a
forall a. Ord a => TypeError a -> a
forall m. Monoid m => TypeError m -> m
forall a. TypeError a -> Bool
forall a. TypeError a -> Int
forall a. TypeError a -> [a]
forall a. (a -> a -> a) -> TypeError a -> a
forall m a. Monoid m => (a -> m) -> TypeError a -> m
forall b a. (b -> a -> b) -> b -> TypeError a -> b
forall a b. (a -> b -> b) -> b -> TypeError a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => TypeError a -> a
$cproduct :: forall a. Num a => TypeError a -> a
sum :: forall a. Num a => TypeError a -> a
$csum :: forall a. Num a => TypeError a -> a
minimum :: forall a. Ord a => TypeError a -> a
$cminimum :: forall a. Ord a => TypeError a -> a
maximum :: forall a. Ord a => TypeError a -> a
$cmaximum :: forall a. Ord a => TypeError a -> a
elem :: forall a. Eq a => a -> TypeError a -> Bool
$celem :: forall a. Eq a => a -> TypeError a -> Bool
length :: forall a. TypeError a -> Int
$clength :: forall a. TypeError a -> Int
null :: forall a. TypeError a -> Bool
$cnull :: forall a. TypeError a -> Bool
toList :: forall a. TypeError a -> [a]
$ctoList :: forall a. TypeError a -> [a]
foldl1 :: forall a. (a -> a -> a) -> TypeError a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> TypeError a -> a
foldr1 :: forall a. (a -> a -> a) -> TypeError a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> TypeError a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> TypeError a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> TypeError a -> b
foldl :: forall b a. (b -> a -> b) -> b -> TypeError a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> TypeError a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> TypeError a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> TypeError a -> b
foldr :: forall a b. (a -> b -> b) -> b -> TypeError a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> TypeError a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> TypeError a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> TypeError a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> TypeError a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> TypeError a -> m
fold :: forall m. Monoid m => TypeError m -> m
$cfold :: forall m. Monoid m => TypeError m -> m
Foldable)

makeBaseFunctor ''TypeError

instance Substitutable (TypeError a) where
  apply :: Subst -> TypeError a -> TypeError a
apply Subst
s = forall t a. Recursive t => (Base t a -> a) -> t -> a
cata forall a. TypeErrorF a (TypeError a) -> TypeError a
go
    where
      go :: TypeErrorF a (TypeError a) -> TypeError a
      go :: forall a. TypeErrorF a (TypeError a) -> TypeError a
go TypeErrorF a (TypeError a)
teF = forall t. Corecursive t => Base t t -> t
embed forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Substitutable a => Subst -> a -> a
apply Subst
s) TypeErrorF a (TypeError a)
teF

  ftv :: TypeError a -> Set TV
ftv TypeError a
_ = forall a. Set a
Set.empty

getLocFromErr :: TypeError a -> [Location a]
getLocFromErr :: forall a. TypeError a -> [Location a]
getLocFromErr = forall {b}. [b] -> [(b, b)]
go forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (:) []
  where
    go :: [b] -> [(b, b)]
go = \case
      [] -> []
      (b
x : b
y : [b]
xs) -> (b
x, b
y) forall a. a -> [a] -> [a]
: [b] -> [(b, b)]
go [b]
xs
      [b]
_ -> forall a. HasCallStack => a
undefined

getLocFromErrs :: [TypeError b] -> [Location b]
getLocFromErrs :: forall b. [TypeError b] -> [Location b]
getLocFromErrs = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a. TypeError a -> [Location a]
getLocFromErr

getTypeClassFromErr :: TypeError a -> Set.Set TypeClass
getTypeClassFromErr :: forall a. TypeError a -> Set TypeClass
getTypeClassFromErr = \case
  UnificationFail Set TypeClass
tyCls InfernoType
_ InfernoType
_ Location a
_ -> Set TypeClass
tyCls
  ExpectedFunction Set TypeClass
tyCls InfernoType
_ InfernoType
_ Location a
_ -> Set TypeClass
tyCls
  ImplicitVarTypeOverlap Set TypeClass
tyCls ExtIdent
_ InfernoType
_ InfernoType
_ Location a
_ -> Set TypeClass
tyCls
  IfConditionMustBeBool Set TypeClass
tyCls InfernoType
_ Location a
_ -> Set TypeClass
tyCls
  AssertConditionMustBeBool Set TypeClass
tyCls InfernoType
_ Location a
_ -> Set TypeClass
tyCls
  IfBranchesMustBeEqType Set TypeClass
tyCls InfernoType
_ InfernoType
_ Location a
_ Location a
_ -> Set TypeClass
tyCls
  CaseBranchesMustBeEqType Set TypeClass
tyCls InfernoType
_ InfernoType
_ Location a
_ Location a
_ -> Set TypeClass
tyCls
  PatternsMustBeEqType Set TypeClass
tyCls InfernoType
_ InfernoType
_ Pat (Pinned VCObjectHash) a
_ Pat (Pinned VCObjectHash) a
_ Location a
_ Location a
_ -> Set TypeClass
tyCls
  TypeError a
_ -> forall a. Monoid a => a
mempty

getTypeClassFromErrs :: [TypeError a] -> Set.Set TypeClass
getTypeClassFromErrs :: forall a. [TypeError a] -> Set TypeClass
getTypeClassFromErrs = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. Ord a => Set a -> Set a -> Set a
Set.union forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. TypeError a -> Set TypeClass
getTypeClassFromErr