{-# LANGUAGE DeriveAnyClass     #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DerivingStrategies #-}
-- | This module contains types for type errors.
module Type.Check.HM.TypeError where

import Control.DeepSeq (NFData)
import Data.Data
import Data.Function (on)
import GHC.Generics    (Generic)
import Type.Check.HM.Type
import Type.Check.HM.Subst

import qualified Data.List as L

-- | Type errors.
data TypeError loc var
  = OccursErr  loc (Type loc var)                 -- ^ error of mismatch of polymorphic constructors, infinite type. Like [a] = a
  | UnifyErr   loc (Type loc var) (Type loc var)  -- ^ Unification error
  | SubtypeErr loc (Type loc var) (Type loc var)  -- ^ Subtype error (happens on explicit type assertions)
  | NotInScopeErr loc var                         -- ^ Missing signature in context for free-variable.
  | ConsArityMismatch
      { TypeError loc var -> loc
consArityMismatch'loc :: loc
      , TypeError loc var -> var
consArityMismatch'tag :: var
      , TypeError loc var -> Int
consArityMismatch'expected :: Int
      , TypeError loc var -> Int
consArityMismatch'actual   :: Int
      } -- ^ mismatch of arity in pattern-matching
  | EmptyCaseExpr loc                             -- ^ no case alternatives in the case expression
  | FreshNameFound                                -- ^ internal error with fresh name substitution. Should not normally occur if algorithm is correct.
  deriving stock    (Int -> TypeError loc var -> ShowS
[TypeError loc var] -> ShowS
TypeError loc var -> String
(Int -> TypeError loc var -> ShowS)
-> (TypeError loc var -> String)
-> ([TypeError loc var] -> ShowS)
-> Show (TypeError loc var)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall loc var.
(Show loc, Show var) =>
Int -> TypeError loc var -> ShowS
forall loc var.
(Show loc, Show var) =>
[TypeError loc var] -> ShowS
forall loc var. (Show loc, Show var) => TypeError loc var -> String
showList :: [TypeError loc var] -> ShowS
$cshowList :: forall loc var.
(Show loc, Show var) =>
[TypeError loc var] -> ShowS
show :: TypeError loc var -> String
$cshow :: forall loc var. (Show loc, Show var) => TypeError loc var -> String
showsPrec :: Int -> TypeError loc var -> ShowS
$cshowsPrec :: forall loc var.
(Show loc, Show var) =>
Int -> TypeError loc var -> ShowS
Show, TypeError loc var -> TypeError loc var -> Bool
(TypeError loc var -> TypeError loc var -> Bool)
-> (TypeError loc var -> TypeError loc var -> Bool)
-> Eq (TypeError loc var)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall loc var.
(Eq loc, Eq var) =>
TypeError loc var -> TypeError loc var -> Bool
/= :: TypeError loc var -> TypeError loc var -> Bool
$c/= :: forall loc var.
(Eq loc, Eq var) =>
TypeError loc var -> TypeError loc var -> Bool
== :: TypeError loc var -> TypeError loc var -> Bool
$c== :: forall loc var.
(Eq loc, Eq var) =>
TypeError loc var -> TypeError loc var -> Bool
Eq, a -> TypeError loc b -> TypeError loc a
(a -> b) -> TypeError loc a -> TypeError loc b
(forall a b. (a -> b) -> TypeError loc a -> TypeError loc b)
-> (forall a b. a -> TypeError loc b -> TypeError loc a)
-> Functor (TypeError loc)
forall a b. a -> TypeError loc b -> TypeError loc a
forall a b. (a -> b) -> TypeError loc a -> TypeError loc b
forall loc a b. a -> TypeError loc b -> TypeError loc a
forall loc a b. (a -> b) -> TypeError loc a -> TypeError loc b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> TypeError loc b -> TypeError loc a
$c<$ :: forall loc a b. a -> TypeError loc b -> TypeError loc a
fmap :: (a -> b) -> TypeError loc a -> TypeError loc b
$cfmap :: forall loc a b. (a -> b) -> TypeError loc a -> TypeError loc b
Functor, (forall x. TypeError loc var -> Rep (TypeError loc var) x)
-> (forall x. Rep (TypeError loc var) x -> TypeError loc var)
-> Generic (TypeError loc var)
forall x. Rep (TypeError loc var) x -> TypeError loc var
forall x. TypeError loc var -> Rep (TypeError loc var) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall loc var x. Rep (TypeError loc var) x -> TypeError loc var
forall loc var x. TypeError loc var -> Rep (TypeError loc var) x
$cto :: forall loc var x. Rep (TypeError loc var) x -> TypeError loc var
$cfrom :: forall loc var x. TypeError loc var -> Rep (TypeError loc var) x
Generic, Typeable (TypeError loc var)
DataType
Constr
Typeable (TypeError loc var)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g)
    -> TypeError loc var
    -> c (TypeError loc var))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (TypeError loc var))
-> (TypeError loc var -> Constr)
-> (TypeError loc var -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (TypeError loc var)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (TypeError loc var)))
-> ((forall b. Data b => b -> b)
    -> TypeError loc var -> TypeError loc var)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> TypeError loc var -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> TypeError loc var -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> TypeError loc var -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> TypeError loc var -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> TypeError loc var -> m (TypeError loc var))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> TypeError loc var -> m (TypeError loc var))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> TypeError loc var -> m (TypeError loc var))
-> Data (TypeError loc var)
TypeError loc var -> DataType
TypeError loc var -> Constr
(forall b. Data b => b -> b)
-> TypeError loc var -> TypeError loc var
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> TypeError loc var
-> c (TypeError loc var)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TypeError loc var)
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (TypeError loc var))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> TypeError loc var -> u
forall u. (forall d. Data d => d -> u) -> TypeError loc var -> [u]
forall loc var.
(Data loc, Data var) =>
Typeable (TypeError loc var)
forall loc var.
(Data loc, Data var) =>
TypeError loc var -> DataType
forall loc var. (Data loc, Data var) => TypeError loc var -> Constr
forall loc var.
(Data loc, Data var) =>
(forall b. Data b => b -> b)
-> TypeError loc var -> TypeError loc var
forall loc var u.
(Data loc, Data var) =>
Int -> (forall d. Data d => d -> u) -> TypeError loc var -> u
forall loc var u.
(Data loc, Data var) =>
(forall d. Data d => d -> u) -> TypeError loc var -> [u]
forall loc var r r'.
(Data loc, Data var) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypeError loc var -> r
forall loc var r r'.
(Data loc, Data var) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TypeError loc var -> r
forall loc var (m :: * -> *).
(Data loc, Data var, Monad m) =>
(forall d. Data d => d -> m d)
-> TypeError loc var -> m (TypeError loc var)
forall loc var (m :: * -> *).
(Data loc, Data var, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> TypeError loc var -> m (TypeError loc var)
forall loc var (c :: * -> *).
(Data loc, Data var) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TypeError loc var)
forall loc var (c :: * -> *).
(Data loc, Data var) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> TypeError loc var
-> c (TypeError loc var)
forall loc var (t :: * -> *) (c :: * -> *).
(Data loc, Data var, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (TypeError loc var))
forall loc var (t :: * -> * -> *) (c :: * -> *).
(Data loc, Data var, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (TypeError loc var))
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypeError loc var -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TypeError loc var -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> TypeError loc var -> m (TypeError loc var)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> TypeError loc var -> m (TypeError loc var)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TypeError loc var)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> TypeError loc var
-> c (TypeError loc var)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (TypeError loc var))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (TypeError loc var))
$cFreshNameFound :: Constr
$cEmptyCaseExpr :: Constr
$cConsArityMismatch :: Constr
$cNotInScopeErr :: Constr
$cSubtypeErr :: Constr
$cUnifyErr :: Constr
$cOccursErr :: Constr
$tTypeError :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> TypeError loc var -> m (TypeError loc var)
$cgmapMo :: forall loc var (m :: * -> *).
(Data loc, Data var, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> TypeError loc var -> m (TypeError loc var)
gmapMp :: (forall d. Data d => d -> m d)
-> TypeError loc var -> m (TypeError loc var)
$cgmapMp :: forall loc var (m :: * -> *).
(Data loc, Data var, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> TypeError loc var -> m (TypeError loc var)
gmapM :: (forall d. Data d => d -> m d)
-> TypeError loc var -> m (TypeError loc var)
$cgmapM :: forall loc var (m :: * -> *).
(Data loc, Data var, Monad m) =>
(forall d. Data d => d -> m d)
-> TypeError loc var -> m (TypeError loc var)
gmapQi :: Int -> (forall d. Data d => d -> u) -> TypeError loc var -> u
$cgmapQi :: forall loc var u.
(Data loc, Data var) =>
Int -> (forall d. Data d => d -> u) -> TypeError loc var -> u
gmapQ :: (forall d. Data d => d -> u) -> TypeError loc var -> [u]
$cgmapQ :: forall loc var u.
(Data loc, Data var) =>
(forall d. Data d => d -> u) -> TypeError loc var -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TypeError loc var -> r
$cgmapQr :: forall loc var r r'.
(Data loc, Data var) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TypeError loc var -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypeError loc var -> r
$cgmapQl :: forall loc var r r'.
(Data loc, Data var) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TypeError loc var -> r
gmapT :: (forall b. Data b => b -> b)
-> TypeError loc var -> TypeError loc var
$cgmapT :: forall loc var.
(Data loc, Data var) =>
(forall b. Data b => b -> b)
-> TypeError loc var -> TypeError loc var
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (TypeError loc var))
$cdataCast2 :: forall loc var (t :: * -> * -> *) (c :: * -> *).
(Data loc, Data var, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (TypeError loc var))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (TypeError loc var))
$cdataCast1 :: forall loc var (t :: * -> *) (c :: * -> *).
(Data loc, Data var, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (TypeError loc var))
dataTypeOf :: TypeError loc var -> DataType
$cdataTypeOf :: forall loc var.
(Data loc, Data var) =>
TypeError loc var -> DataType
toConstr :: TypeError loc var -> Constr
$ctoConstr :: forall loc var. (Data loc, Data var) => TypeError loc var -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TypeError loc var)
$cgunfold :: forall loc var (c :: * -> *).
(Data loc, Data var) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TypeError loc var)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> TypeError loc var
-> c (TypeError loc var)
$cgfoldl :: forall loc var (c :: * -> *).
(Data loc, Data var) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> TypeError loc var
-> c (TypeError loc var)
$cp1Data :: forall loc var.
(Data loc, Data var) =>
Typeable (TypeError loc var)
Data)
  deriving anyclass (TypeError loc var -> ()
(TypeError loc var -> ()) -> NFData (TypeError loc var)
forall a. (a -> ()) -> NFData a
forall loc var. (NFData loc, NFData var) => TypeError loc var -> ()
rnf :: TypeError loc var -> ()
$crnf :: forall loc var. (NFData loc, NFData var) => TypeError loc var -> ()
NFData)

instance LocFunctor TypeError where
  mapLoc :: (locA -> locB) -> TypeError locA var -> TypeError locB var
mapLoc locA -> locB
f = \case
    OccursErr locA
loc Type locA var
ty     -> locB -> Type locB var -> TypeError locB var
forall loc var. loc -> Type loc var -> TypeError loc var
OccursErr (locA -> locB
f locA
loc) ((locA -> locB) -> Type locA var -> Type locB var
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc locA -> locB
f Type locA var
ty)
    UnifyErr locA
loc Type locA var
tA Type locA var
tB   -> locB -> Type locB var -> Type locB var -> TypeError locB var
forall loc var.
loc -> Type loc var -> Type loc var -> TypeError loc var
UnifyErr (locA -> locB
f locA
loc) ((locA -> locB) -> Type locA var -> Type locB var
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc locA -> locB
f Type locA var
tA) ((locA -> locB) -> Type locA var -> Type locB var
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc locA -> locB
f Type locA var
tB)
    SubtypeErr locA
loc Type locA var
tA Type locA var
tB -> locB -> Type locB var -> Type locB var -> TypeError locB var
forall loc var.
loc -> Type loc var -> Type loc var -> TypeError loc var
SubtypeErr (locA -> locB
f locA
loc) ((locA -> locB) -> Type locA var -> Type locB var
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc locA -> locB
f Type locA var
tA) ((locA -> locB) -> Type locA var -> Type locB var
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc locA -> locB
f Type locA var
tB)
    NotInScopeErr locA
loc var
v  -> locB -> var -> TypeError locB var
forall loc var. loc -> var -> TypeError loc var
NotInScopeErr (locA -> locB
f locA
loc) var
v
    ConsArityMismatch locA
loc var
tag Int
expect Int
actual -> locB -> var -> Int -> Int -> TypeError locB var
forall loc var. loc -> var -> Int -> Int -> TypeError loc var
ConsArityMismatch (locA -> locB
f locA
loc)  var
tag Int
expect Int
actual
    EmptyCaseExpr locA
loc    -> locB -> TypeError locB var
forall loc var. loc -> TypeError loc var
EmptyCaseExpr (locA -> locB
f locA
loc)
    TypeError locA var
FreshNameFound       -> TypeError locB var
forall loc var. TypeError loc var
FreshNameFound

instance HasTypeVars TypeError where
  tyVars :: TypeError src var -> VarSet src var
tyVars = \case
    OccursErr src
_ Type src var
ty     -> Type src var -> VarSet src var
forall (f :: * -> * -> *) var src.
(HasTypeVars f, Ord var) =>
f src var -> VarSet src var
tyVars Type src var
ty
    UnifyErr src
_ Type src var
a Type src var
b     -> Type src var -> VarSet src var
forall (f :: * -> * -> *) var src.
(HasTypeVars f, Ord var) =>
f src var -> VarSet src var
tyVars Type src var
a VarSet src var -> VarSet src var -> VarSet src var
forall a. Semigroup a => a -> a -> a
<> Type src var -> VarSet src var
forall (f :: * -> * -> *) var src.
(HasTypeVars f, Ord var) =>
f src var -> VarSet src var
tyVars Type src var
b
    SubtypeErr src
_ Type src var
a Type src var
b   -> Type src var -> VarSet src var
forall (f :: * -> * -> *) var src.
(HasTypeVars f, Ord var) =>
f src var -> VarSet src var
tyVars Type src var
a VarSet src var -> VarSet src var -> VarSet src var
forall a. Semigroup a => a -> a -> a
<> Type src var -> VarSet src var
forall (f :: * -> * -> *) var src.
(HasTypeVars f, Ord var) =>
f src var -> VarSet src var
tyVars Type src var
b
    NotInScopeErr src
_ var
_  -> VarSet src var
forall a. Monoid a => a
mempty
    ConsArityMismatch src
_ var
_ Int
_ Int
_ -> VarSet src var
forall a. Monoid a => a
mempty
    EmptyCaseExpr src
_    -> VarSet src var
forall a. Monoid a => a
mempty
    TypeError src var
FreshNameFound     -> VarSet src var
forall a. Monoid a => a
mempty

  tyVarsInOrder :: TypeError src var -> [(var, src)]
tyVarsInOrder TypeError src var
err = ((var, src) -> (var, src) -> Bool) -> [(var, src)] -> [(var, src)]
forall a. (a -> a -> Bool) -> [a] -> [a]
L.nubBy (var -> var -> Bool
forall a. Eq a => a -> a -> Bool
(==) (var -> var -> Bool)
-> ((var, src) -> var) -> (var, src) -> (var, src) -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (var, src) -> var
forall a b. (a, b) -> a
fst) ([(var, src)] -> [(var, src)]) -> [(var, src)] -> [(var, src)]
forall a b. (a -> b) -> a -> b
$ case TypeError src var
err of
    OccursErr src
_ Type src var
ty     -> Type src var -> [(var, src)]
forall (f :: * -> * -> *) src var.
(HasTypeVars f, Eq src, Ord var) =>
f src var -> [(var, src)]
tyVarsInOrder Type src var
ty
    UnifyErr src
_ Type src var
a Type src var
b     -> Type src var -> [(var, src)]
forall (f :: * -> * -> *) src var.
(HasTypeVars f, Eq src, Ord var) =>
f src var -> [(var, src)]
tyVarsInOrder Type src var
a [(var, src)] -> [(var, src)] -> [(var, src)]
forall a. Semigroup a => a -> a -> a
<> Type src var -> [(var, src)]
forall (f :: * -> * -> *) src var.
(HasTypeVars f, Eq src, Ord var) =>
f src var -> [(var, src)]
tyVarsInOrder Type src var
b
    SubtypeErr src
_ Type src var
a Type src var
b   -> Type src var -> [(var, src)]
forall (f :: * -> * -> *) src var.
(HasTypeVars f, Eq src, Ord var) =>
f src var -> [(var, src)]
tyVarsInOrder Type src var
a [(var, src)] -> [(var, src)] -> [(var, src)]
forall a. Semigroup a => a -> a -> a
<> Type src var -> [(var, src)]
forall (f :: * -> * -> *) src var.
(HasTypeVars f, Eq src, Ord var) =>
f src var -> [(var, src)]
tyVarsInOrder Type src var
b
    NotInScopeErr src
_ var
_  -> [(var, src)]
forall a. Monoid a => a
mempty
    EmptyCaseExpr src
_    -> [(var, src)]
forall a. Monoid a => a
mempty
    TypeError src var
FreshNameFound     -> [(var, src)]
forall a. Monoid a => a
mempty
    ConsArityMismatch src
_ var
_ Int
_ Int
_ -> [(var, src)]
forall a. Monoid a => a
mempty

instance CanApply TypeError where
  apply :: Subst loc v -> TypeError loc v -> TypeError loc v
apply Subst loc v
f = \case
    OccursErr loc
loc Type loc v
ty   -> loc -> Type loc v -> TypeError loc v
forall loc var. loc -> Type loc var -> TypeError loc var
OccursErr loc
loc (Type loc v -> TypeError loc v) -> Type loc v -> TypeError loc v
forall a b. (a -> b) -> a -> b
$ Subst loc v -> Type loc v -> Type loc v
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst loc v
f Type loc v
ty
    UnifyErr loc
loc Type loc v
a Type loc v
b   -> loc -> Type loc v -> Type loc v -> TypeError loc v
forall loc var.
loc -> Type loc var -> Type loc var -> TypeError loc var
UnifyErr loc
loc (Subst loc v -> Type loc v -> Type loc v
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst loc v
f Type loc v
a) (Subst loc v -> Type loc v -> Type loc v
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst loc v
f Type loc v
b)
    SubtypeErr loc
loc Type loc v
a Type loc v
b -> loc -> Type loc v -> Type loc v -> TypeError loc v
forall loc var.
loc -> Type loc var -> Type loc var -> TypeError loc var
SubtypeErr loc
loc (Subst loc v -> Type loc v -> Type loc v
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst loc v
f Type loc v
a) (Subst loc v -> Type loc v -> Type loc v
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst loc v
f Type loc v
b)
    TypeError loc v
other              -> TypeError loc v
other