{-# LANGUAGE DeriveFunctor     #-}
{-# LANGUAGE OverloadedStrings #-}

module Ty ( Subst
          , runTyM, tyP
          , match, aT
          , tyOf
          ) where

import           A
import           Control.Exception                (Exception, throw)
import           Control.Monad                    (zipWithM)
import           Control.Monad.Except             (liftEither, throwError)
import           Control.Monad.Trans.State.Strict (StateT, gets, modify, runState, runStateT, state)
import           Data.Bifunctor                   (first, second)
import           Data.Foldable                    (traverse_)
import           Data.Function                    (on)
import           Data.Functor                     (void, ($>))
import qualified Data.IntMap                      as IM
import qualified Data.IntSet                      as IS
import qualified Data.Set                         as S
import qualified Data.Text                        as T
import           Data.Typeable                    (Typeable)
import qualified Data.Vector                      as V
import           Nm
import qualified Nm.Map                           as Nm
import           Prettyprinter                    (Pretty (..), squotes, (<+>))
import           Ty.Const
import           U

data Err a = UF a T T | MF T T
           | Doesn'tSatisfy a T C
           | IllScoped a (Nm a)
           | Ambiguous T (E ())
           | IllScopedTyVar (TyName ())
           | Occ a T T
           deriving (forall a b. (a -> b) -> Err a -> Err b)
-> (forall a b. a -> Err b -> Err a) -> Functor Err
forall a b. a -> Err b -> Err a
forall a b. (a -> b) -> Err a -> Err b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Err a -> Err b
fmap :: forall a b. (a -> b) -> Err a -> Err b
$c<$ :: forall a b. a -> Err b -> Err a
<$ :: forall a b. a -> Err b -> Err a
Functor

instance Pretty a => Pretty (Err a) where
    pretty :: forall ann. Err a -> Doc ann
pretty (UF a
l T
ty T
ty')           = a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
l Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"could not unify type" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (T -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. T -> Doc ann
pretty T
ty) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"with" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (T -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. T -> Doc ann
pretty T
ty')
    pretty (Doesn'tSatisfy a
l T
ty C
c) = a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
l Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (T -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. T -> Doc ann
pretty T
ty) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"is not a member of class" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> C -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. C -> Doc ann
pretty C
c
    pretty (IllScoped a
l Nm a
n)         = a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
l Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (Nm a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Nm a -> Doc ann
pretty Nm a
n) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"is not in scope."
    pretty (Ambiguous T
ty E ()
e)        = Doc ann
"type" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (T -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. T -> Doc ann
pretty T
ty) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"of" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (E () -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. E () -> Doc ann
pretty E ()
e) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"is ambiguous"
    pretty (IllScopedTyVar TyName ()
n)      = Doc ann
"Type variable" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (TyName () -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. TyName () -> Doc ann
pretty TyName ()
n) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"is not in scope."
    pretty (MF T
t T
t')               = Doc ann
"Failed to match" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (T -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. T -> Doc ann
pretty T
t) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"against type" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (T -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. T -> Doc ann
pretty T
t')
    pretty (Occ a
l T
t T
t')            = a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
l Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"occurs check failed when unifying type" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (T -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. T -> Doc ann
pretty T
t) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"with type" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (T -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. T -> Doc ann
pretty T
t')

instance Pretty a => Show (Err a) where show :: Err a -> String
show=Doc Any -> String
forall a. Show a => a -> String
show(Doc Any -> String) -> (Err a -> Doc Any) -> Err a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Err a -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Err a -> Doc ann
pretty

instance (Typeable a, Pretty a) => Exception (Err a) where

data TyState a = TyState { forall a. TyState a -> Int
maxU      :: !Int
                         , forall a. TyState a -> IntMap (Set (C, a))
classVars :: IM.IntMap (S.Set (C, a))
                         , forall a. TyState a -> IntMap T
varEnv    :: IM.IntMap T
                         }

setMaxU :: Int -> TyState a -> TyState a
setMaxU :: forall a. Int -> TyState a -> TyState a
setMaxU Int
i (TyState Int
_ IntMap (Set (C, a))
c IntMap T
v) = Int -> IntMap (Set (C, a)) -> IntMap T -> TyState a
forall a. Int -> IntMap (Set (C, a)) -> IntMap T -> TyState a
TyState Int
i IntMap (Set (C, a))
c IntMap T
v

addCM :: Ord a => Nm b -> (C, a) -> TyM a ()
addCM :: forall a b. Ord a => Nm b -> (C, a) -> TyM a ()
addCM Nm b
tv (C, a)
c = (TyState a -> TyState a) -> StateT (TyState a) (Either (Err a)) ()
forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify ((IntMap (Set (C, a)) -> IntMap (Set (C, a)))
-> TyState a -> TyState a
forall a.
(IntMap (Set (C, a)) -> IntMap (Set (C, a)))
-> TyState a -> TyState a
mapCV (Nm b -> (C, a) -> IntMap (Set (C, a)) -> IntMap (Set (C, a))
forall a b.
Ord a =>
Nm b -> (C, a) -> IntMap (Set (C, a)) -> IntMap (Set (C, a))
addC Nm b
tv (C, a)
c))

mapCV :: (IM.IntMap (S.Set (C, a)) -> IM.IntMap (S.Set (C, a))) -> TyState a -> TyState a
mapCV :: forall a.
(IntMap (Set (C, a)) -> IntMap (Set (C, a)))
-> TyState a -> TyState a
mapCV IntMap (Set (C, a)) -> IntMap (Set (C, a))
f (TyState Int
u IntMap (Set (C, a))
cvs IntMap T
v) = Int -> IntMap (Set (C, a)) -> IntMap T -> TyState a
forall a. Int -> IntMap (Set (C, a)) -> IntMap T -> TyState a
TyState Int
u (IntMap (Set (C, a)) -> IntMap (Set (C, a))
f IntMap (Set (C, a))
cvs) IntMap T
v

addVarEnv :: Int -> T -> TyState a -> TyState a
addVarEnv :: forall a. Int -> T -> TyState a -> TyState a
addVarEnv Int
i T
ty (TyState Int
u IntMap (Set (C, a))
cvs IntMap T
v) = Int -> IntMap (Set (C, a)) -> IntMap T -> TyState a
forall a. Int -> IntMap (Set (C, a)) -> IntMap T -> TyState a
TyState Int
u IntMap (Set (C, a))
cvs (Int -> T -> IntMap T -> IntMap T
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
i T
ty IntMap T
v)

addVarM :: Int -> T -> TyM a ()
addVarM :: forall a. Int -> T -> TyM a ()
addVarM Int
i T
ty = (TyState a -> TyState a) -> StateT (TyState a) (Either (Err a)) ()
forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify (Int -> T -> TyState a -> TyState a
forall a. Int -> T -> TyState a -> TyState a
addVarEnv Int
i T
ty)

type TyM a = StateT (TyState a) (Either (Err a))

runTyM :: Int -> TyM a b -> Either (Err a) (b, Int)
runTyM :: forall a b. Int -> TyM a b -> Either (Err a) (b, Int)
runTyM Int
i = ((b, TyState a) -> (b, Int))
-> Either (Err a) (b, TyState a) -> Either (Err a) (b, Int)
forall a b. (a -> b) -> Either (Err a) a -> Either (Err a) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TyState a -> Int) -> (b, TyState a) -> (b, Int)
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 TyState a -> Int
forall a. TyState a -> Int
maxU) (Either (Err a) (b, TyState a) -> Either (Err a) (b, Int))
-> (TyM a b -> Either (Err a) (b, TyState a))
-> TyM a b
-> Either (Err a) (b, Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyM a b -> TyState a -> Either (Err a) (b, TyState a))
-> TyState a -> TyM a b -> Either (Err a) (b, TyState a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip TyM a b -> TyState a -> Either (Err a) (b, TyState a)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Int -> IntMap (Set (C, a)) -> IntMap T -> TyState a
forall a. Int -> IntMap (Set (C, a)) -> IntMap T -> TyState a
TyState Int
i IntMap (Set (C, a))
forall a. IntMap a
IM.empty IntMap T
forall a. IntMap a
IM.empty)

type Subst = IM.IntMap T

aT :: Subst -> T -> T
aT :: IntMap T -> T -> T
aT IntMap T
um ty' :: T
ty'@(TyVar (Nm Text
_ (U Int
i) ()
_)) =
    case Int -> IntMap T -> Maybe T
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
i IntMap T
um of
        Just ty :: T
ty@TyVar{} -> IntMap T -> T -> T
aT (Int -> IntMap T -> IntMap T
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
i IntMap T
um) T
ty -- prevent cyclic lookups
        Just ty :: T
ty@Rho{}   -> IntMap T -> T -> T
aT (Int -> IntMap T -> IntMap T
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
i IntMap T
um) T
ty
        Just ty :: T
ty@Ρ{}     -> IntMap T -> T -> T
aT (Int -> IntMap T -> IntMap T
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
i IntMap T
um) T
ty
        Just T
ty         -> IntMap T -> T -> T
aT IntMap T
um T
ty
        Maybe T
Nothing         -> T
ty'
aT IntMap T
um (Rho n :: TyName ()
n@(Nm Text
_ (U Int
i) ()
_) IntMap T
rs) =
    case Int -> IntMap T -> Maybe T
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
i IntMap T
um of
        Just ty :: T
ty@Rho{}   -> IntMap T -> T -> T
aT (Int -> IntMap T -> IntMap T
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
i IntMap T
um) T
ty
        Just ty :: T
ty@Ρ{}     -> IntMap T -> T -> T
aT (Int -> IntMap T -> IntMap T
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
i IntMap T
um) T
ty
        Just ty :: T
ty@TyVar{} -> IntMap T -> T -> T
aT (Int -> IntMap T -> IntMap T
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
i IntMap T
um) T
ty
        Just T
ty         -> IntMap T -> T -> T
aT IntMap T
um T
ty
        Maybe T
Nothing         -> TyName () -> IntMap T -> T
Rho TyName ()
n ((T -> T) -> IntMap T -> IntMap T
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IntMap T -> T -> T
aT IntMap T
um) IntMap T
rs)
aT IntMap T
um (Ρ n :: TyName ()
n@(Nm Text
_ (U Int
i) ()
_) NmMap T
rs) =
    case Int -> IntMap T -> Maybe T
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
i IntMap T
um of
        Just ty :: T
ty@Ρ{}     -> IntMap T -> T -> T
aT (Int -> IntMap T -> IntMap T
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
i IntMap T
um) T
ty
        Just ty :: T
ty@TyVar{} -> IntMap T -> T -> T
aT (Int -> IntMap T -> IntMap T
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
i IntMap T
um) T
ty
        Just ty :: T
ty@Rho{}   -> IntMap T -> T -> T
aT (Int -> IntMap T -> IntMap T
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
i IntMap T
um) T
ty
        Just T
ty         -> IntMap T -> T -> T
aT IntMap T
um T
ty
        Maybe T
Nothing         -> TyName () -> NmMap T -> T
Ρ TyName ()
n ((T -> T) -> NmMap T -> NmMap T
forall a b. (a -> b) -> NmMap a -> NmMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IntMap T -> T -> T
aT IntMap T
um) NmMap T
rs)
aT IntMap T
_ ty' :: T
ty'@TyB{} = T
ty'
aT IntMap T
um (T
ty:$T
ty') = IntMap T -> T -> T
aT IntMap T
um T
ty T -> T -> T
:$ IntMap T -> T -> T
aT IntMap T
um T
ty'
aT IntMap T
um (TyArr T
ty T
ty') = T -> T -> T
TyArr (IntMap T -> T -> T
aT IntMap T
um T
ty) (IntMap T -> T -> T
aT IntMap T
um T
ty')
aT IntMap T
um (TyTup [T]
tys)    = [T] -> T
TyTup (IntMap T -> T -> T
aT IntMap T
um (T -> T) -> [T] -> [T]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [T]
tys)
aT IntMap T
um (TyRec NmMap T
tys)    = NmMap T -> T
TyRec (IntMap T -> T -> T
aT IntMap T
um (T -> T) -> NmMap T -> NmMap T
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NmMap T
tys)

mguPrep :: l -> Subst -> T -> T -> Either (Err l) Subst
mguPrep :: forall l. l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
mguPrep l
l IntMap T
s = l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
forall l. l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
mgu l
l IntMap T
s (T -> T -> Either (Err l) (IntMap T))
-> (T -> T) -> T -> T -> Either (Err l) (IntMap T)
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` IntMap T -> T -> T
aT IntMap T
s

match :: T -> T -> Subst
match :: T -> T -> IntMap T
match T
t T
t' = (Err () -> IntMap T)
-> (IntMap T -> IntMap T) -> Either (Err ()) (IntMap T) -> IntMap T
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Err () -> IntMap T
forall a e. (?callStack::CallStack, Exception e) => e -> a
throw :: Err () -> Subst) IntMap T -> IntMap T
forall a. a -> a
id (T -> T -> Either (Err ()) (IntMap T)
forall l. T -> T -> Either (Err l) (IntMap T)
maM T
t T
t')

maM :: T -> T -> Either (Err l) Subst
maM :: forall l. T -> T -> Either (Err l) (IntMap T)
maM (TyB TB
b) (TyB TB
b') | TB
b TB -> TB -> Bool
forall a. Eq a => a -> a -> Bool
== TB
b' = IntMap T -> Either (Err l) (IntMap T)
forall a b. b -> Either a b
Right IntMap T
forall a. Monoid a => a
mempty
maM (TyVar TyName ()
n) (TyVar TyName ()
n') | TyName ()
n TyName () -> TyName () -> Bool
forall a. Eq a => a -> a -> Bool
== TyName ()
n' = IntMap T -> Either (Err l) (IntMap T)
forall a b. b -> Either a b
Right IntMap T
forall a. Monoid a => a
mempty
maM (TyVar (Nm Text
_ (U Int
i) ()
_)) T
t = IntMap T -> Either (Err l) (IntMap T)
forall a b. b -> Either a b
Right (Int -> T -> IntMap T
forall a. Int -> a -> IntMap a
IM.singleton Int
i T
t)
maM (TyArr T
t0 T
t1) (TyArr T
t0' T
t1') = IntMap T -> IntMap T -> IntMap T
forall a. Semigroup a => a -> a -> a
(<>) (IntMap T -> IntMap T -> IntMap T)
-> Either (Err l) (IntMap T)
-> Either (Err l) (IntMap T -> IntMap T)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> T -> T -> Either (Err l) (IntMap T)
forall l. T -> T -> Either (Err l) (IntMap T)
maM T
t0 T
t0' Either (Err l) (IntMap T -> IntMap T)
-> Either (Err l) (IntMap T) -> Either (Err l) (IntMap T)
forall a b.
Either (Err l) (a -> b) -> Either (Err l) a -> Either (Err l) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> T -> T -> Either (Err l) (IntMap T)
forall l. T -> T -> Either (Err l) (IntMap T)
maM T
t1' T
t1 -- TODO: I think <> is right
maM (TyTup [T]
ts) (TyTup [T]
ts') = ([IntMap T] -> IntMap T)
-> Either (Err l) [IntMap T] -> Either (Err l) (IntMap T)
forall a b. (a -> b) -> Either (Err l) a -> Either (Err l) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [IntMap T] -> IntMap T
forall a. Monoid a => [a] -> a
mconcat ((T -> T -> Either (Err l) (IntMap T))
-> [T] -> [T] -> Either (Err l) [IntMap T]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM T -> T -> Either (Err l) (IntMap T)
forall l. T -> T -> Either (Err l) (IntMap T)
maM [T]
ts [T]
ts')
maM (Rho TyName ()
n IntMap T
_) (Rho TyName ()
n' IntMap T
_) | TyName ()
n TyName () -> TyName () -> Bool
forall a. Eq a => a -> a -> Bool
== TyName ()
n' = IntMap T -> Either (Err l) (IntMap T)
forall a b. b -> Either a b
Right IntMap T
forall a. Monoid a => a
mempty
maM (Rho TyName ()
n IntMap T
rs) t :: T
t@(Rho TyName ()
_ IntMap T
rs') | IntMap T -> IntSet
forall a. IntMap a -> IntSet
IM.keysSet IntMap T
rs' IntSet -> IntSet -> Bool
`IS.isSubsetOf` IntMap T -> IntSet
forall a. IntMap a -> IntSet
IM.keysSet IntMap T
rs
    = Int -> T -> IntMap T -> IntMap T
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert (U -> Int
unU(U -> Int) -> U -> Int
forall a b. (a -> b) -> a -> b
$TyName () -> U
forall a. Nm a -> U
unique TyName ()
n) T
t (IntMap T -> IntMap T)
-> ([IntMap T] -> IntMap T) -> [IntMap T] -> IntMap T
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [IntMap T] -> IntMap T
forall a. Monoid a => [a] -> a
mconcat ([IntMap T] -> IntMap T)
-> Either (Err l) [IntMap T] -> Either (Err l) (IntMap T)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((T, T) -> Either (Err l) (IntMap T))
-> [(T, T)] -> Either (Err l) [IntMap T]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((T -> T -> Either (Err l) (IntMap T))
-> (T, T) -> Either (Err l) (IntMap T)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry T -> T -> Either (Err l) (IntMap T)
forall l. T -> T -> Either (Err l) (IntMap T)
maM) (IntMap (T, T) -> [(T, T)]
forall a. IntMap a -> [a]
IM.elems ((T -> T -> (T, T)) -> IntMap T -> IntMap T -> IntMap (T, T)
forall a b c. (a -> b -> c) -> IntMap a -> IntMap b -> IntMap c
IM.intersectionWith (,) IntMap T
rs IntMap T
rs'))
maM (Rho TyName ()
n IntMap T
rs) t :: T
t@(TyTup [T]
ts) | [T] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [T]
ts Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= (Int, T) -> Int
forall a b. (a, b) -> a
fst (IntMap T -> (Int, T)
forall a. IntMap a -> (Int, a)
IM.findMax IntMap T
rs)
    = Int -> T -> IntMap T -> IntMap T
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert (U -> Int
unU(U -> Int) -> U -> Int
forall a b. (a -> b) -> a -> b
$TyName () -> U
forall a. Nm a -> U
unique TyName ()
n) T
t (IntMap T -> IntMap T)
-> ([IntMap T] -> IntMap T) -> [IntMap T] -> IntMap T
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [IntMap T] -> IntMap T
forall a. Monoid a => [a] -> a
mconcat ([IntMap T] -> IntMap T)
-> Either (Err l) [IntMap T] -> Either (Err l) (IntMap T)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((T, T) -> Either (Err l) (IntMap T))
-> [(T, T)] -> Either (Err l) [IntMap T]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((T -> T -> Either (Err l) (IntMap T))
-> (T, T) -> Either (Err l) (IntMap T)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry T -> T -> Either (Err l) (IntMap T)
forall l. T -> T -> Either (Err l) (IntMap T)
maM) [ ([T]
ts[T] -> Int -> T
forall a. (?callStack::CallStack) => [a] -> Int -> a
!!(Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1),T
tϵ) | (Int
i,T
tϵ) <- IntMap T -> [(Int, T)]
forall a. IntMap a -> [(Int, a)]
IM.toList IntMap T
rs ]
maM T
t T
t' = Err l -> Either (Err l) (IntMap T)
forall a b. a -> Either a b
Left (Err l -> Either (Err l) (IntMap T))
-> Err l -> Either (Err l) (IntMap T)
forall a b. (a -> b) -> a -> b
$ T -> T -> Err l
forall a. T -> T -> Err a
MF T
t T
t'

occ :: T -> IS.IntSet
occ :: T -> IntSet
occ (TyVar (Nm Text
_ (U Int
i) ()
_))  = Int -> IntSet
IS.singleton Int
i
occ TyB{}                   = IntSet
IS.empty
occ (TyTup [T]
ts)              = (T -> IntSet) -> [T] -> IntSet
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap T -> IntSet
occ [T]
ts
occ (TyRec NmMap T
ts)              = (T -> IntSet) -> NmMap T -> IntSet
forall m a. Monoid m => (a -> m) -> NmMap a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap T -> IntSet
occ NmMap T
ts
occ (T
t:$T
t')                 = T -> IntSet
occ T
t IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<> T -> IntSet
occ T
t'
occ (TyArr T
t T
t')            = T -> IntSet
occ T
t IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<> T -> IntSet
occ T
t'
occ (Rho (Nm Text
_ (U Int
i) ()
_) IntMap T
rs) = Int -> IntSet -> IntSet
IS.insert Int
i ((T -> IntSet) -> [T] -> IntSet
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap T -> IntSet
occ (IntMap T -> [T]
forall a. IntMap a -> [a]
IM.elems IntMap T
rs))
occ (Ρ (Nm Text
_ (U Int
i) ()
_) NmMap T
rs)   = Int -> IntSet -> IntSet
IS.insert Int
i ((T -> IntSet) -> [T] -> IntSet
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap T -> IntSet
occ (NmMap T -> [T]
forall a. NmMap a -> [a]
Nm.elems NmMap T
rs))

mgu :: l -> Subst -> T -> T -> Either (Err l) Subst
mgu :: forall l. l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
mgu l
_ IntMap T
s (TyB TB
b) (TyB TB
b') | TB
b TB -> TB -> Bool
forall a. Eq a => a -> a -> Bool
== TB
b' = IntMap T -> Either (Err l) (IntMap T)
forall a b. b -> Either a b
Right IntMap T
s
mgu l
_ IntMap T
s (TyVar TyName ()
n) (TyVar TyName ()
n') | TyName ()
n TyName () -> TyName () -> Bool
forall a. Eq a => a -> a -> Bool
== TyName ()
n' = IntMap T -> Either (Err l) (IntMap T)
forall a b. b -> Either a b
Right IntMap T
s
mgu l
l IntMap T
s T
t t' :: T
t'@(TyVar (Nm Text
_ (U Int
k) ()
_)) | Int
k Int -> IntSet -> Bool
`IS.notMember` T -> IntSet
occ T
t = IntMap T -> Either (Err l) (IntMap T)
forall a b. b -> Either a b
Right (IntMap T -> Either (Err l) (IntMap T))
-> IntMap T -> Either (Err l) (IntMap T)
forall a b. (a -> b) -> a -> b
$ Int -> T -> IntMap T -> IntMap T
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
k T
t IntMap T
s
                                      | Bool
otherwise = Err l -> Either (Err l) (IntMap T)
forall a b. a -> Either a b
Left (Err l -> Either (Err l) (IntMap T))
-> Err l -> Either (Err l) (IntMap T)
forall a b. (a -> b) -> a -> b
$ l -> T -> T -> Err l
forall a. a -> T -> T -> Err a
Occ l
l T
t' T
t
mgu l
l IntMap T
s t :: T
t@(TyVar (Nm Text
_ (U Int
k) ()
_)) T
t' | Int
k Int -> IntSet -> Bool
`IS.notMember` T -> IntSet
occ T
t' = IntMap T -> Either (Err l) (IntMap T)
forall a b. b -> Either a b
Right (IntMap T -> Either (Err l) (IntMap T))
-> IntMap T -> Either (Err l) (IntMap T)
forall a b. (a -> b) -> a -> b
$ Int -> T -> IntMap T -> IntMap T
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
k T
t' IntMap T
s
                                      | Bool
otherwise = Err l -> Either (Err l) (IntMap T)
forall a b. a -> Either a b
Left (Err l -> Either (Err l) (IntMap T))
-> Err l -> Either (Err l) (IntMap T)
forall a b. (a -> b) -> a -> b
$ l -> T -> T -> Err l
forall a. a -> T -> T -> Err a
Occ l
l T
t T
t'
mgu l
l IntMap T
s (TyArr T
t0 T
t1) (TyArr T
t0' T
t1')  = do {s0 <- l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
forall l. l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
mgu l
l IntMap T
s T
t0 T
t0'; mguPrep l s0 t1 t1'}
mgu l
l IntMap T
s (T
t0:$T
t1) (T
t0':$T
t1')            = do {s0 <- l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
forall l. l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
mgu l
l IntMap T
s T
t0 T
t0'; mguPrep l s0 t1 t1'}
mgu l
l IntMap T
s (TyTup [T]
ts) (TyTup [T]
ts') | [T] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [T]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [T] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [T]
ts' = (IntMap T -> T -> T -> Either (Err l) (IntMap T))
-> IntMap T -> [T] -> [T] -> Either (Err l) (IntMap T)
forall {f :: * -> *} {t} {t} {t}.
Monad f =>
(t -> t -> t -> f t) -> t -> [t] -> [t] -> f t
zS (l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
forall l. l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
mguPrep l
l) IntMap T
s [T]
ts [T]
ts'
mgu l
l IntMap T
s (Rho TyName ()
n IntMap T
rs) t' :: T
t'@(TyTup [T]
ts) | [T] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [T]
ts Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= (Int, T) -> Int
forall a b. (a, b) -> a
fst (IntMap T -> (Int, T)
forall a. IntMap a -> (Int, a)
IM.findMax IntMap T
rs) Bool -> Bool -> Bool
&& (Int, T) -> Int
forall a b. (a, b) -> a
fst (IntMap T -> (Int, T)
forall a. IntMap a -> (Int, a)
IM.findMin IntMap T
rs) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0
    = (IntMap T -> (Int, T) -> Either (Err l) (IntMap T))
-> IntMap T -> [(Int, T)] -> Either (Err l) (IntMap T)
forall (m :: * -> *) b.
Monad m =>
(IntMap T -> b -> m (IntMap T)) -> IntMap T -> [b] -> m (IntMap T)
tS_ (\IntMap T
sϵ (Int
i, T
tϵ) -> Int -> T -> IntMap T -> IntMap T
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert (U -> Int
unU(U -> Int) -> U -> Int
forall a b. (a -> b) -> a -> b
$TyName () -> U
forall a. Nm a -> U
unique TyName ()
n) T
t' (IntMap T -> IntMap T)
-> Either (Err l) (IntMap T) -> Either (Err l) (IntMap T)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
forall l. l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
mguPrep l
l IntMap T
sϵ ([T]
ts[T] -> Int -> T
forall a. (?callStack::CallStack) => [a] -> Int -> a
!!(Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)) T
tϵ) IntMap T
s (IntMap T -> [(Int, T)]
forall a. IntMap a -> [(Int, a)]
IM.toList IntMap T
rs)
mgu l
l IntMap T
s (Ρ TyName ()
n NmMap T
rs) t' :: T
t'@(TyRec NmMap T
ts) | NmMap T
rs NmMap T -> NmMap T -> Bool
forall a b. NmMap a -> NmMap b -> Bool
`Nm.isSubmapOf` NmMap T
rs
    = (IntMap T -> (TyName (), T) -> Either (Err l) (IntMap T))
-> IntMap T -> [(TyName (), T)] -> Either (Err l) (IntMap T)
forall (m :: * -> *) b.
Monad m =>
(IntMap T -> b -> m (IntMap T)) -> IntMap T -> [b] -> m (IntMap T)
tS_ (\IntMap T
sϵ (TyName ()
nr, T
tϵ) -> Int -> T -> IntMap T -> IntMap T
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert (U -> Int
unU(U -> Int) -> U -> Int
forall a b. (a -> b) -> a -> b
$TyName () -> U
forall a. Nm a -> U
unique TyName ()
n) T
t' (IntMap T -> IntMap T)
-> Either (Err l) (IntMap T) -> Either (Err l) (IntMap T)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
forall l. l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
mguPrep l
l IntMap T
sϵ (NmMap T
ts NmMap T -> TyName () -> T
forall a b. NmMap a -> Nm b -> a
Nm.! TyName ()
nr) T
tϵ) IntMap T
s (NmMap T -> [(TyName (), T)]
forall a. NmMap a -> [(TyName (), a)]
Nm.toList NmMap T
rs)
mgu l
l IntMap T
s t :: T
t@TyTup{} t' :: T
t'@Rho{} = l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
forall l. l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
mgu l
l IntMap T
s T
t' T
t
mgu l
l IntMap T
s t :: T
t@TyRec{} t' :: T
t'@Ρ{} = l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
forall l. l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
mgu l
l IntMap T
s T
t' T
t
mgu l
l IntMap T
s (TyRec NmMap T
ts) (TyRec NmMap T
ts') | NmMap T
ts NmMap T -> NmMap T -> Bool
forall a b. NmMap a -> NmMap b -> Bool
`Nm.isSubmapOf` NmMap T
ts' Bool -> Bool -> Bool
&& NmMap T
ts' NmMap T -> NmMap T -> Bool
forall a b. NmMap a -> NmMap b -> Bool
`Nm.isSubmapOf` NmMap T
ts
    = (IntMap T -> (T, T) -> Either (Err l) (IntMap T))
-> IntMap T -> [(T, T)] -> Either (Err l) (IntMap T)
forall (m :: * -> *) b.
Monad m =>
(IntMap T -> b -> m (IntMap T)) -> IntMap T -> [b] -> m (IntMap T)
tS_ (\IntMap T
sϵ (T
t0,T
t1) -> l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
forall l. l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
mguPrep l
l IntMap T
sϵ T
t0 T
t1) IntMap T
s ([(T, T)] -> Either (Err l) (IntMap T))
-> [(T, T)] -> Either (Err l) (IntMap T)
forall a b. (a -> b) -> a -> b
$ NmMap (T, T) -> [(T, T)]
forall a. NmMap a -> [a]
Nm.elems (NmMap (T, T) -> [(T, T)]) -> NmMap (T, T) -> [(T, T)]
forall a b. (a -> b) -> a -> b
$ (T -> T -> (T, T)) -> NmMap T -> NmMap T -> NmMap (T, T)
forall a b c. (a -> b -> c) -> NmMap a -> NmMap b -> NmMap c
Nm.intersectionWith (,) NmMap T
ts NmMap T
ts'
mgu l
l IntMap T
s (Rho TyName ()
n IntMap T
rs) (Rho TyName ()
n' IntMap T
rs') = do
    rss <- (IntMap T -> (T, T) -> Either (Err l) (IntMap T))
-> IntMap T -> [(T, T)] -> Either (Err l) (IntMap T)
forall (m :: * -> *) b.
Monad m =>
(IntMap T -> b -> m (IntMap T)) -> IntMap T -> [b] -> m (IntMap T)
tS_ (\IntMap T
sϵ (T
t0,T
t1) -> l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
forall l. l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
mguPrep l
l IntMap T
sϵ T
t0 T
t1) IntMap T
s ([(T, T)] -> Either (Err l) (IntMap T))
-> [(T, T)] -> Either (Err l) (IntMap T)
forall a b. (a -> b) -> a -> b
$ IntMap (T, T) -> [(T, T)]
forall a. IntMap a -> [a]
IM.elems (IntMap (T, T) -> [(T, T)]) -> IntMap (T, T) -> [(T, T)]
forall a b. (a -> b) -> a -> b
$ (T -> T -> (T, T)) -> IntMap T -> IntMap T -> IntMap (T, T)
forall a b c. (a -> b -> c) -> IntMap a -> IntMap b -> IntMap c
IM.intersectionWith (,) IntMap T
rs IntMap T
rs'
    pure (IM.insert (unU$unique n) (Rho n' (rs <> rs')) rss)
mgu l
l IntMap T
s (Ρ TyName ()
n NmMap T
rs) (Ρ TyName ()
n' NmMap T
rs') = do
    rss <- (IntMap T -> (T, T) -> Either (Err l) (IntMap T))
-> IntMap T -> [(T, T)] -> Either (Err l) (IntMap T)
forall (m :: * -> *) b.
Monad m =>
(IntMap T -> b -> m (IntMap T)) -> IntMap T -> [b] -> m (IntMap T)
tS_ (\IntMap T
sϵ (T
t0,T
t1) -> l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
forall l. l -> IntMap T -> T -> T -> Either (Err l) (IntMap T)
mguPrep l
l IntMap T
sϵ T
t0 T
t1) IntMap T
s ([(T, T)] -> Either (Err l) (IntMap T))
-> [(T, T)] -> Either (Err l) (IntMap T)
forall a b. (a -> b) -> a -> b
$ NmMap (T, T) -> [(T, T)]
forall a. NmMap a -> [a]
Nm.elems (NmMap (T, T) -> [(T, T)]) -> NmMap (T, T) -> [(T, T)]
forall a b. (a -> b) -> a -> b
$ (T -> T -> (T, T)) -> NmMap T -> NmMap T -> NmMap (T, T)
forall a b c. (a -> b -> c) -> NmMap a -> NmMap b -> NmMap c
Nm.intersectionWith (,) NmMap T
rs NmMap T
rs'
    pure (IM.insert (unU$unique n) (Ρ n' (rs <> rs')) rss)
mgu l
l IntMap T
_ T
t T
t' = Err l -> Either (Err l) (IntMap T)
forall a b. a -> Either a b
Left (Err l -> Either (Err l) (IntMap T))
-> Err l -> Either (Err l) (IntMap T)
forall a b. (a -> b) -> a -> b
$ l -> T -> T -> Err l
forall a. a -> T -> T -> Err a
UF l
l T
t T
t'

tS_ :: Monad m => (Subst -> b -> m Subst) -> Subst -> [b] -> m Subst
tS_ :: forall (m :: * -> *) b.
Monad m =>
(IntMap T -> b -> m (IntMap T)) -> IntMap T -> [b] -> m (IntMap T)
tS_ IntMap T -> b -> m (IntMap T)
_ IntMap T
s []     = IntMap T -> m (IntMap T)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure IntMap T
s
tS_ IntMap T -> b -> m (IntMap T)
f IntMap T
s (b
t:[b]
ts) = do {next <- IntMap T -> b -> m (IntMap T)
f IntMap T
s b
t; tS_ f next ts}

zS :: (t -> t -> t -> f t) -> t -> [t] -> [t] -> f t
zS t -> t -> t -> f t
_ t
s [] [t]
_           = t -> f t
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
s
zS t -> t -> t -> f t
_ t
s [t]
_ []           = t -> f t
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
s
zS t -> t -> t -> f t
op t
s (t
x:[t]
xs) (t
y:[t]
ys) = do {next <- t -> t -> t -> f t
op t
s t
x t
y; zS op next xs ys}

substInt :: IM.IntMap T -> Int -> Maybe T
substInt :: IntMap T -> Int -> Maybe T
substInt IntMap T
tys Int
k =
    case Int -> IntMap T -> Maybe T
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
k IntMap T
tys of
        Just ty' :: T
ty'@TyVar{}     -> T -> Maybe T
forall a. a -> Maybe a
Just (T -> Maybe T) -> T -> Maybe T
forall a b. (a -> b) -> a -> b
$ IntMap T -> T -> T
aT (Int -> IntMap T -> IntMap T
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
k IntMap T
tys) T
ty'
        Just (T
ty0:$T
ty1)      -> T -> Maybe T
forall a. a -> Maybe a
Just (T -> Maybe T) -> T -> Maybe T
forall a b. (a -> b) -> a -> b
$ let tys' :: IntMap T
tys'=Int -> IntMap T -> IntMap T
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
k IntMap T
tys in IntMap T -> T -> T
aT IntMap T
tys' T
ty0 T -> T -> T
:$ IntMap T -> T -> T
aT IntMap T
tys' T
ty1
        Just (TyArr T
ty0 T
ty1) -> T -> Maybe T
forall a. a -> Maybe a
Just (T -> Maybe T) -> T -> Maybe T
forall a b. (a -> b) -> a -> b
$ let tys' :: IntMap T
tys'=Int -> IntMap T -> IntMap T
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
k IntMap T
tys in T -> T -> T
TyArr (IntMap T -> T -> T
aT IntMap T
tys' T
ty0) (IntMap T -> T -> T
aT IntMap T
tys' T
ty1)
        Just (TyTup [T]
tysϵ)    -> T -> Maybe T
forall a. a -> Maybe a
Just (T -> Maybe T) -> T -> Maybe T
forall a b. (a -> b) -> a -> b
$ let tys' :: IntMap T
tys'=Int -> IntMap T -> IntMap T
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
k IntMap T
tys in [T] -> T
TyTup (IntMap T -> T -> T
aT IntMap T
tys'(T -> T) -> [T] -> [T]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>[T]
tysϵ)
        Just (TyRec NmMap T
tysϵ)    -> T -> Maybe T
forall a. a -> Maybe a
Just (T -> Maybe T) -> T -> Maybe T
forall a b. (a -> b) -> a -> b
$ let tys' :: IntMap T
tys'=Int -> IntMap T -> IntMap T
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
k IntMap T
tys in NmMap T -> T
TyRec (IntMap T -> T -> T
aT IntMap T
tys'(T -> T) -> NmMap T -> NmMap T
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>NmMap T
tysϵ)
        Just ty' :: T
ty'@Rho{}       -> T -> Maybe T
forall a. a -> Maybe a
Just (T -> Maybe T) -> T -> Maybe T
forall a b. (a -> b) -> a -> b
$ IntMap T -> T -> T
aT (Int -> IntMap T -> IntMap T
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
k IntMap T
tys) T
ty'
        Just ty' :: T
ty'@Ρ{}         -> T -> Maybe T
forall a. a -> Maybe a
Just (T -> Maybe T) -> T -> Maybe T
forall a b. (a -> b) -> a -> b
$ IntMap T -> T -> T
aT (Int -> IntMap T -> IntMap T
forall a. Int -> IntMap a -> IntMap a
IM.delete Int
k IntMap T
tys) T
ty'
        Just T
ty'             -> T -> Maybe T
forall a. a -> Maybe a
Just T
ty'
        Maybe T
Nothing              -> Maybe T
forall a. Maybe a
Nothing

freshN :: T.Text -> TyM a (Nm ())
freshN :: forall a. Text -> TyM a (TyName ())
freshN Text
n = (TyState a -> (TyName (), TyState a))
-> StateT (TyState a) (Either (Err a)) (TyName ())
forall (m :: * -> *) s a. Monad m => (s -> (a, s)) -> StateT s m a
state (\TyState a
st -> let j :: Int
j=TyState a -> Int
forall a. TyState a -> Int
maxU TyState a
stInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1 in (Text -> U -> () -> TyName ()
forall a. Text -> U -> a -> Nm a
Nm Text
n (Int -> U
U Int
j) (), TyState a
st { maxU = j }))

freshTV :: T.Text -> TyM a T
freshTV :: forall a. Text -> TyM a T
freshTV=(TyName () -> T)
-> StateT (TyState a) (Either (Err a)) (TyName ())
-> StateT (TyState a) (Either (Err a)) T
forall a b.
(a -> b)
-> StateT (TyState a) (Either (Err a)) a
-> StateT (TyState a) (Either (Err a)) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TyName () -> T
var(StateT (TyState a) (Either (Err a)) (TyName ())
 -> StateT (TyState a) (Either (Err a)) T)
-> (Text -> StateT (TyState a) (Either (Err a)) (TyName ()))
-> Text
-> StateT (TyState a) (Either (Err a)) T
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Text -> StateT (TyState a) (Either (Err a)) (TyName ())
forall a. Text -> TyM a (TyName ())
freshN

addC :: Ord a => Nm b -> (C, a) -> IM.IntMap (S.Set (C, a)) -> IM.IntMap (S.Set (C, a))
addC :: forall a b.
Ord a =>
Nm b -> (C, a) -> IntMap (Set (C, a)) -> IntMap (Set (C, a))
addC (Nm Text
_ (U Int
i) b
_) (C, a)
c = (Maybe (Set (C, a)) -> Maybe (Set (C, a)))
-> Int -> IntMap (Set (C, a)) -> IntMap (Set (C, a))
forall a. (Maybe a -> Maybe a) -> Int -> IntMap a -> IntMap a
IM.alter (Set (C, a) -> Maybe (Set (C, a))
forall a. a -> Maybe a
Just (Set (C, a) -> Maybe (Set (C, a)))
-> (Maybe (Set (C, a)) -> Set (C, a))
-> Maybe (Set (C, a))
-> Maybe (Set (C, a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (Set (C, a)) -> Set (C, a)
go) Int
i where
    go :: Maybe (Set (C, a)) -> Set (C, a)
go Maybe (Set (C, a))
Nothing   = (C, a) -> Set (C, a)
forall a. a -> Set a
S.singleton (C, a)
c
    go (Just Set (C, a)
cs) = (C, a) -> Set (C, a) -> Set (C, a)
forall a. Ord a => a -> Set a -> Set a
S.insert (C, a)
c Set (C, a)
cs

tyArr :: T -> T -> T
tyArr :: T -> T -> T
tyArr = T -> T -> T
TyArr

var :: Nm () -> T
var :: TyName () -> T
var = TyName () -> T
TyVar

liftCloneTy :: T -> TyM b T
liftCloneTy :: forall b. T -> TyM b T
liftCloneTy T
ty = do
    i <- (TyState b -> Int) -> StateT (TyState b) (Either (Err b)) Int
forall (m :: * -> *) s a. Monad m => (s -> a) -> StateT s m a
gets TyState b -> Int
forall a. TyState a -> Int
maxU
    let (ty', (j, iMaps)) = cloneTy i ty
    -- FIXME: clone/propagate constraints
    ty' <$ modify (setMaxU j)

cloneTy :: Int -> T -> (T, (Int, IM.IntMap U))
cloneTy :: Int -> T -> (T, (Int, IntMap U))
cloneTy Int
i T
ty = (State (Int, IntMap U) T
 -> (Int, IntMap U) -> (T, (Int, IntMap U)))
-> (Int, IntMap U)
-> State (Int, IntMap U) T
-> (T, (Int, IntMap U))
forall a b c. (a -> b -> c) -> b -> a -> c
flip State (Int, IntMap U) T -> (Int, IntMap U) -> (T, (Int, IntMap U))
forall s a. State s a -> s -> (a, s)
runState (Int
i, IntMap U
forall a. IntMap a
IM.empty) (State (Int, IntMap U) T -> (T, (Int, IntMap U)))
-> State (Int, IntMap U) T -> (T, (Int, IntMap U))
forall a b. (a -> b) -> a -> b
$ T -> State (Int, IntMap U) T
forall {m :: * -> *}. Monad m => T -> StateT (Int, IntMap U) m T
cloneTyM T
ty
    where cloneTyM :: T -> StateT (Int, IntMap U) m T
cloneTyM (TyVar (Nm Text
n (U Int
j) ()
l')) = do
                st <- ((Int, IntMap U) -> IntMap U)
-> StateT (Int, IntMap U) m (IntMap U)
forall (m :: * -> *) s a. Monad m => (s -> a) -> StateT s m a
gets (Int, IntMap U) -> IntMap U
forall a b. (a, b) -> b
snd
                case IM.lookup j st of
                    Just U
k -> T -> StateT (Int, IntMap U) m T
forall a. a -> StateT (Int, IntMap U) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyName () -> T
TyVar (Text -> U -> () -> TyName ()
forall a. Text -> U -> a -> Nm a
Nm Text
n U
k ()
l'))
                    Maybe U
Nothing -> ((Int, IntMap U) -> (T, (Int, IntMap U)))
-> StateT (Int, IntMap U) m T
forall (m :: * -> *) s a. Monad m => (s -> (a, s)) -> StateT s m a
state (((Int, IntMap U) -> (T, (Int, IntMap U)))
 -> StateT (Int, IntMap U) m T)
-> ((Int, IntMap U) -> (T, (Int, IntMap U)))
-> StateT (Int, IntMap U) m T
forall a b. (a -> b) -> a -> b
$ \(Int
k, IntMap U
b) ->
                        let j' :: Int
j'=Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1; u :: U
u=Int -> U
U Int
j'
                        in (TyName () -> T
TyVar (Text -> U -> () -> TyName ()
forall a. Text -> U -> a -> Nm a
Nm Text
n U
u ()
l'), (Int
j', Int -> U -> IntMap U -> IntMap U
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
j U
u IntMap U
b))
          cloneTyM (TyArr T
tyϵ T
ty')               = T -> T -> T
TyArr (T -> T -> T)
-> StateT (Int, IntMap U) m T -> StateT (Int, IntMap U) m (T -> T)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> T -> StateT (Int, IntMap U) m T
cloneTyM T
tyϵ StateT (Int, IntMap U) m (T -> T)
-> StateT (Int, IntMap U) m T -> StateT (Int, IntMap U) m T
forall a b.
StateT (Int, IntMap U) m (a -> b)
-> StateT (Int, IntMap U) m a -> StateT (Int, IntMap U) m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> T -> StateT (Int, IntMap U) m T
cloneTyM T
ty'
          cloneTyM (T
tyϵ:$T
ty')                    = T -> T -> T
(:$) (T -> T -> T)
-> StateT (Int, IntMap U) m T -> StateT (Int, IntMap U) m (T -> T)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> T -> StateT (Int, IntMap U) m T
cloneTyM T
tyϵ StateT (Int, IntMap U) m (T -> T)
-> StateT (Int, IntMap U) m T -> StateT (Int, IntMap U) m T
forall a b.
StateT (Int, IntMap U) m (a -> b)
-> StateT (Int, IntMap U) m a -> StateT (Int, IntMap U) m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> T -> StateT (Int, IntMap U) m T
cloneTyM T
ty'
          cloneTyM (TyTup [T]
tys)                   = [T] -> T
TyTup ([T] -> T)
-> StateT (Int, IntMap U) m [T] -> StateT (Int, IntMap U) m T
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (T -> StateT (Int, IntMap U) m T)
-> [T] -> StateT (Int, IntMap U) m [T]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse T -> StateT (Int, IntMap U) m T
cloneTyM [T]
tys
          cloneTyM (TyRec NmMap T
tys)                   = NmMap T -> T
TyRec (NmMap T -> T)
-> StateT (Int, IntMap U) m (NmMap T) -> StateT (Int, IntMap U) m T
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (T -> StateT (Int, IntMap U) m T)
-> NmMap T -> StateT (Int, IntMap U) m (NmMap T)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NmMap a -> f (NmMap b)
traverse T -> StateT (Int, IntMap U) m T
cloneTyM NmMap T
tys
          cloneTyM (Rho TyName ()
n IntMap T
tys)                   = TyName () -> IntMap T -> T
Rho TyName ()
n (IntMap T -> T)
-> StateT (Int, IntMap U) m (IntMap T)
-> StateT (Int, IntMap U) m T
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (T -> StateT (Int, IntMap U) m T)
-> IntMap T -> StateT (Int, IntMap U) m (IntMap T)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> IntMap a -> f (IntMap b)
traverse T -> StateT (Int, IntMap U) m T
cloneTyM IntMap T
tys
          cloneTyM (Ρ TyName ()
n NmMap T
tys)                     = TyName () -> NmMap T -> T
Ρ TyName ()
n (NmMap T -> T)
-> StateT (Int, IntMap U) m (NmMap T) -> StateT (Int, IntMap U) m T
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (T -> StateT (Int, IntMap U) m T)
-> NmMap T -> StateT (Int, IntMap U) m (NmMap T)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NmMap a -> f (NmMap b)
traverse T -> StateT (Int, IntMap U) m T
cloneTyM NmMap T
tys
          cloneTyM tyϵ :: T
tyϵ@TyB{}                     = T -> StateT (Int, IntMap U) m T
forall a. a -> StateT (Int, IntMap U) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure T
tyϵ

checkType :: Ord a => T -> (C, a) -> TyM a ()
checkType :: forall a. Ord a => T -> (C, a) -> TyM a ()
checkType TyVar{} (C, a)
_                      = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyStr) (C
IsSemigroup, a
_)   = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyI) (C
IsSemigroup, a
_)     = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyFloat) (C
IsSemigroup, a
_) = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyI) (C
IsNum, a
_)           = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyFloat) (C
IsNum, a
_)       = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyI) (C
IsEq, a
_)            = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyFloat) (C
IsEq, a
_)        = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyBool) (C
IsEq, a
_)         = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyStr) (C
IsEq, a
_)          = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyTup [T]
tys) (c :: C
c@C
IsEq, a
l)        = (T -> StateT (TyState a) (Either (Err a)) ())
-> [T] -> StateT (TyState a) (Either (Err a)) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (T -> (C, a) -> StateT (TyState a) (Either (Err a)) ()
forall a. Ord a => T -> (C, a) -> TyM a ()
`checkType` (C
c, a
l)) [T]
tys
checkType (TyRec NmMap T
tys) (c :: C
c@C
IsEq, a
l)        = (T -> StateT (TyState a) (Either (Err a)) ())
-> NmMap T -> StateT (TyState a) (Either (Err a)) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (T -> (C, a) -> StateT (TyState a) (Either (Err a)) ()
forall a. Ord a => T -> (C, a) -> TyM a ()
`checkType` (C
c, a
l)) NmMap T
tys
checkType (Rho TyName ()
_ IntMap T
rs) (c :: C
c@C
IsEq, a
l)         = (T -> StateT (TyState a) (Either (Err a)) ())
-> [T] -> StateT (TyState a) (Either (Err a)) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (T -> (C, a) -> StateT (TyState a) (Either (Err a)) ()
forall a. Ord a => T -> (C, a) -> TyM a ()
`checkType` (C
c, a
l)) (IntMap T -> [T]
forall a. IntMap a -> [a]
IM.elems IntMap T
rs)
checkType (Ρ TyName ()
_ NmMap T
rs) (c :: C
c@C
IsEq, a
l)           = (T -> StateT (TyState a) (Either (Err a)) ())
-> [T] -> StateT (TyState a) (Either (Err a)) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (T -> (C, a) -> StateT (TyState a) (Either (Err a)) ()
forall a. Ord a => T -> (C, a) -> TyM a ()
`checkType` (C
c, a
l)) (NmMap T -> [T]
forall a. NmMap a -> [a]
Nm.elems NmMap T
rs)
checkType (TyB TB
TyVec:$T
ty) (c :: C
c@C
IsEq, a
l)    = T -> (C, a) -> StateT (TyState a) (Either (Err a)) ()
forall a. Ord a => T -> (C, a) -> TyM a ()
checkType T
ty (C
c, a
l)
checkType (TyB TB
TyOption:$T
ty) (c :: C
c@C
IsEq, a
l) = T -> (C, a) -> StateT (TyState a) (Either (Err a)) ()
forall a. Ord a => T -> (C, a) -> TyM a ()
checkType T
ty (C
c, a
l)
checkType (TyB TB
TyI) (C
IsParse, a
_)         = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyFloat) (C
IsParse, a
_)     = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyFloat) (C
IsOrd, a
_)       = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyI) (C
IsOrd, a
_)           = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyStr) (C
IsOrd, a
_)         = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyVec) (C
Functor, a
_)       = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyStream) (C
Functor, a
_)    = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyOption) (C
Functor, a
_)    = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyStream) (C
Witherable, a
_) = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyVec) (C
Witherable, a
_)    = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyVec) (C
Foldable, a
_)      = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyStream) (C
Foldable, a
_)   = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyStr) (C
IsMonoid, a
_)      = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyVec:$T
_) (C
IsMonoid, a
_)   = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyStr) (C
IsPrintf, a
_)      = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyFloat) (C
IsPrintf, a
_)    = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyI) (C
IsPrintf, a
_)        = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyB TB
TyBool) (C
IsPrintf, a
_)     = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkType (TyTup [T]
tys) (c :: C
c@C
IsPrintf, a
l)    | Bool -> Bool
not(Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$(T -> Bool) -> [T] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any T -> Bool
nest [T]
tys = (T -> StateT (TyState a) (Either (Err a)) ())
-> [T] -> StateT (TyState a) (Either (Err a)) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (T -> (C, a) -> StateT (TyState a) (Either (Err a)) ()
forall a. Ord a => T -> (C, a) -> TyM a ()
`checkType` (C
c, a
l)) [T]
tys
checkType (TyRec NmMap T
tys) (c :: C
c@C
IsPrintf, a
l)    | [T]
tys' <- NmMap T -> [T]
forall a. NmMap a -> [a]
Nm.elems NmMap T
tys, Bool -> Bool
not(Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$(T -> Bool) -> [T] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any T -> Bool
nest [T]
tys' = (T -> StateT (TyState a) (Either (Err a)) ())
-> [T] -> StateT (TyState a) (Either (Err a)) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (T -> (C, a) -> StateT (TyState a) (Either (Err a)) ()
forall a. Ord a => T -> (C, a) -> TyM a ()
`checkType` (C
c, a
l)) [T]
tys'
checkType (Rho TyName ()
_ IntMap T
rs) (c :: C
c@C
IsPrintf, a
l)     | [T]
tys <- IntMap T -> [T]
forall a. IntMap a -> [a]
IM.elems IntMap T
rs, Bool -> Bool
not(Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$(T -> Bool) -> [T] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any T -> Bool
nest [T]
tys = (T -> StateT (TyState a) (Either (Err a)) ())
-> [T] -> StateT (TyState a) (Either (Err a)) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (T -> (C, a) -> StateT (TyState a) (Either (Err a)) ()
forall a. Ord a => T -> (C, a) -> TyM a ()
`checkType` (C
c, a
l)) [T]
tys
checkType (Ρ TyName ()
_ NmMap T
rs) (c :: C
c@C
IsPrintf, a
l)       | [T]
tys <- NmMap T -> [T]
forall a. NmMap a -> [a]
Nm.elems NmMap T
rs, Bool -> Bool
not(Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$(T -> Bool) -> [T] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any T -> Bool
nest [T]
tys = (T -> StateT (TyState a) (Either (Err a)) ())
-> [T] -> StateT (TyState a) (Either (Err a)) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (T -> (C, a) -> StateT (TyState a) (Either (Err a)) ()
forall a. Ord a => T -> (C, a) -> TyM a ()
`checkType` (C
c, a
l)) [T]
tys
checkType T
ty (C
c, a
l)                      = Err a -> StateT (TyState a) (Either (Err a)) ()
forall a. Err a -> StateT (TyState a) (Either (Err a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Err a -> StateT (TyState a) (Either (Err a)) ())
-> Err a -> StateT (TyState a) (Either (Err a)) ()
forall a b. (a -> b) -> a -> b
$ a -> T -> C -> Err a
forall a. a -> T -> C -> Err a
Doesn'tSatisfy a
l T
ty C
c

nest :: T -> Bool
nest TyTup{}=Bool
True; nest TyRec{}=Bool
True; nest Rho{}=Bool
True; nest Ρ{}=Bool
True; nest T
_=Bool
False

checkClass :: Ord a
           => IM.IntMap T -- ^ Unification result
           -> Int
           -> S.Set (C, a)
           -> TyM a ()
checkClass :: forall a. Ord a => IntMap T -> Int -> Set (C, a) -> TyM a ()
checkClass IntMap T
tys Int
i Set (C, a)
cs = {-# SCC "checkClass" #-}
    case IntMap T -> Int -> Maybe T
substInt IntMap T
tys Int
i of
        Just T
ty -> ((C, a) -> TyM a ()) -> [(C, a)] -> TyM a ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (T -> (C, a) -> TyM a ()
forall a. Ord a => T -> (C, a) -> TyM a ()
checkType T
ty) (Set (C, a) -> [(C, a)]
forall a. Set a -> [a]
S.toList Set (C, a)
cs)
        Maybe T
Nothing -> () -> TyM a ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

lookupVar :: Nm a -> TyM a T
lookupVar :: forall a. Nm a -> TyM a T
lookupVar n :: Nm a
n@(Nm Text
_ (U Int
i) a
l) = do
    st <- (TyState a -> IntMap T)
-> StateT (TyState a) (Either (Err a)) (IntMap T)
forall (m :: * -> *) s a. Monad m => (s -> a) -> StateT s m a
gets TyState a -> IntMap T
forall a. TyState a -> IntMap T
varEnv
    case IM.lookup i st of
        Just T
ty -> T -> StateT (TyState a) (Either (Err a)) T
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure T
ty -- liftCloneTy ty
        Maybe T
Nothing -> Err a -> StateT (TyState a) (Either (Err a)) T
forall a. Err a -> StateT (TyState a) (Either (Err a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Err a -> StateT (TyState a) (Either (Err a)) T)
-> Err a -> StateT (TyState a) (Either (Err a)) T
forall a b. (a -> b) -> a -> b
$ a -> Nm a -> Err a
forall a. a -> Nm a -> Err a
IllScoped a
l Nm a
n

tyOf :: Ord a => E a -> TyM a T
tyOf :: forall a. Ord a => E a -> TyM a T
tyOf = (E T -> T)
-> StateT (TyState a) (Either (Err a)) (E T)
-> StateT (TyState a) (Either (Err a)) T
forall a b.
(a -> b)
-> StateT (TyState a) (Either (Err a)) a
-> StateT (TyState a) (Either (Err a)) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap E T -> T
forall a. E a -> a
eLoc(StateT (TyState a) (Either (Err a)) (E T)
 -> StateT (TyState a) (Either (Err a)) T)
-> (E a -> StateT (TyState a) (Either (Err a)) (E T))
-> E a
-> StateT (TyState a) (Either (Err a)) T
forall b c a. (b -> c) -> (a -> b) -> a -> c
.E a -> StateT (TyState a) (Either (Err a)) (E T)
forall a. Ord a => E a -> TyM a (E T)
tyE

tyDS :: Ord a => Subst -> D a -> TyM a (D T, Subst)
tyDS :: forall a. Ord a => IntMap T -> D a -> TyM a (D T, IntMap T)
tyDS IntMap T
s (SetFS Text
bs)  = (D T, IntMap T)
-> StateT (TyState a) (Either (Err a)) (D T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> D T
forall a. Text -> D a
SetFS Text
bs, IntMap T
s)
tyDS IntMap T
s (SetRS Text
bs)  = (D T, IntMap T)
-> StateT (TyState a) (Either (Err a)) (D T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> D T
forall a. Text -> D a
SetRS Text
bs, IntMap T
s)
tyDS IntMap T
s (SetOFS Text
bs) = (D T, IntMap T)
-> StateT (TyState a) (Either (Err a)) (D T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> D T
forall a. Text -> D a
SetOFS Text
bs, IntMap T
s)
tyDS IntMap T
s (SetORS Text
bs) = (D T, IntMap T)
-> StateT (TyState a) (Either (Err a)) (D T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> D T
forall a. Text -> D a
SetORS Text
bs, IntMap T
s)
tyDS IntMap T
s D a
SetCsv      = (D T, IntMap T)
-> StateT (TyState a) (Either (Err a)) (D T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (D T
forall a. D a
SetCsv, IntMap T
s)
tyDS IntMap T
s D a
SetAsv      = (D T, IntMap T)
-> StateT (TyState a) (Either (Err a)) (D T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (D T
forall a. D a
SetAsv, IntMap T
s)
tyDS IntMap T
s D a
SetUsv      = (D T, IntMap T)
-> StateT (TyState a) (Either (Err a)) (D T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (D T
forall a. D a
SetUsv, IntMap T
s)
tyDS IntMap T
s D a
FlushDecl   = (D T, IntMap T)
-> StateT (TyState a) (Either (Err a)) (D T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (D T
forall a. D a
FlushDecl, IntMap T
s)
tyDS IntMap T
s (FunDecl n :: Nm a
n@(Nm Text
_ (U Int
i) a
_) [] E a
e) = do
    (e', s') <- IntMap T -> E a -> TyM a (E T, IntMap T)
forall a. Ord a => IntMap T -> E a -> TyM a (E T, IntMap T)
tyES IntMap T
s E a
e
    let t=E T -> T
forall a. E a -> a
eLoc E T
e'
    addVarM i t $> (FunDecl (n$>t) [] e', s')
tyDS IntMap T
_ FunDecl{}   = String -> StateT (TyState a) (Either (Err a)) (D T, IntMap T)
forall a. (?callStack::CallStack) => String -> a
error String
"Internal error. Should have been desugared by now."

isAmbiguous :: T -> Bool
isAmbiguous :: T -> Bool
isAmbiguous TyVar{}        = Bool
True
isAmbiguous (TyArr T
ty T
ty') = T -> Bool
isAmbiguous T
ty Bool -> Bool -> Bool
|| T -> Bool
isAmbiguous T
ty'
isAmbiguous (T
ty:$T
ty')      = T -> Bool
isAmbiguous T
ty Bool -> Bool -> Bool
|| T -> Bool
isAmbiguous T
ty'
isAmbiguous (TyTup [T]
tys)    = (T -> Bool) -> [T] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any T -> Bool
isAmbiguous [T]
tys
isAmbiguous (TyRec NmMap T
tys)    = (T -> Bool) -> NmMap T -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any T -> Bool
isAmbiguous NmMap T
tys
isAmbiguous TyB{}          = Bool
False
isAmbiguous Rho{}          = Bool
True
isAmbiguous Ρ{}            = Bool
True

checkAmb :: E T -> TyM a ()
checkAmb :: forall a. E T -> TyM a ()
checkAmb e :: E T
e@(BB T
ty BBin
_) | T -> Bool
isAmbiguous T
ty = Err a -> StateT (TyState a) (Either (Err a)) ()
forall a. Err a -> StateT (TyState a) (Either (Err a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Err a -> StateT (TyState a) (Either (Err a)) ())
-> Err a -> StateT (TyState a) (Either (Err a)) ()
forall a b. (a -> b) -> a -> b
$ T -> E () -> Err a
forall a. T -> E () -> Err a
Ambiguous T
ty (E T -> E ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void E T
e)
checkAmb TB{} = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- don't fail on ternary builtins, we don't need it anyway... better error messages
checkAmb e :: E T
e@(UB T
ty BUn
_) | T -> Bool
isAmbiguous T
ty = Err a -> StateT (TyState a) (Either (Err a)) ()
forall a. Err a -> StateT (TyState a) (Either (Err a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Err a -> StateT (TyState a) (Either (Err a)) ())
-> Err a -> StateT (TyState a) (Either (Err a)) ()
forall a b. (a -> b) -> a -> b
$ T -> E () -> Err a
forall a. T -> E () -> Err a
Ambiguous T
ty (E T -> E ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void E T
e)
checkAmb (Implicit T
_ E T
e') = E T -> StateT (TyState a) (Either (Err a)) ()
forall a. E T -> TyM a ()
checkAmb E T
e'
checkAmb (Guarded T
_ E T
p E T
e') = E T -> StateT (TyState a) (Either (Err a)) ()
forall a. E T -> TyM a ()
checkAmb E T
p StateT (TyState a) (Either (Err a)) ()
-> StateT (TyState a) (Either (Err a)) ()
-> StateT (TyState a) (Either (Err a)) ()
forall a b.
StateT (TyState a) (Either (Err a)) a
-> StateT (TyState a) (Either (Err a)) b
-> StateT (TyState a) (Either (Err a)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> E T -> StateT (TyState a) (Either (Err a)) ()
forall a. E T -> TyM a ()
checkAmb E T
e'
checkAmb (EApp T
_ E T
e' E T
e'') = E T -> StateT (TyState a) (Either (Err a)) ()
forall a. E T -> TyM a ()
checkAmb E T
e' StateT (TyState a) (Either (Err a)) ()
-> StateT (TyState a) (Either (Err a)) ()
-> StateT (TyState a) (Either (Err a)) ()
forall a b.
StateT (TyState a) (Either (Err a)) a
-> StateT (TyState a) (Either (Err a)) b
-> StateT (TyState a) (Either (Err a)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> E T -> StateT (TyState a) (Either (Err a)) ()
forall a. E T -> TyM a ()
checkAmb E T
e'' -- more precise errors
checkAmb (Tup T
_ [E T]
es) = (E T -> StateT (TyState a) (Either (Err a)) ())
-> [E T] -> StateT (TyState a) (Either (Err a)) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ E T -> StateT (TyState a) (Either (Err a)) ()
forall a. E T -> TyM a ()
checkAmb [E T]
es
checkAmb (Rec T
_ [(Nm T, E T)]
es) = ((Nm T, E T) -> StateT (TyState a) (Either (Err a)) ())
-> [(Nm T, E T)] -> StateT (TyState a) (Either (Err a)) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (E T -> StateT (TyState a) (Either (Err a)) ()
forall a. E T -> TyM a ()
checkAmb(E T -> StateT (TyState a) (Either (Err a)) ())
-> ((Nm T, E T) -> E T)
-> (Nm T, E T)
-> StateT (TyState a) (Either (Err a)) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Nm T, E T) -> E T
forall a b. (a, b) -> b
snd) [(Nm T, E T)]
es
checkAmb e :: E T
e@(Arr T
ty Vector (E T)
_) | T -> Bool
isAmbiguous T
ty = Err a -> StateT (TyState a) (Either (Err a)) ()
forall a. Err a -> StateT (TyState a) (Either (Err a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Err a -> StateT (TyState a) (Either (Err a)) ())
-> Err a -> StateT (TyState a) (Either (Err a)) ()
forall a b. (a -> b) -> a -> b
$ T -> E () -> Err a
forall a. T -> E () -> Err a
Ambiguous T
ty (E T -> E ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void E T
e)
checkAmb e :: E T
e@(Var T
ty Nm T
_) | T -> Bool
isAmbiguous T
ty = Err a -> StateT (TyState a) (Either (Err a)) ()
forall a. Err a -> StateT (TyState a) (Either (Err a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Err a -> StateT (TyState a) (Either (Err a)) ())
-> Err a -> StateT (TyState a) (Either (Err a)) ()
forall a b. (a -> b) -> a -> b
$ T -> E () -> Err a
forall a. T -> E () -> Err a
Ambiguous T
ty (E T -> E ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void E T
e)
checkAmb (Let T
_ (Nm T, E T)
bs E T
e) = (E T -> StateT (TyState a) (Either (Err a)) ())
-> [E T] -> StateT (TyState a) (Either (Err a)) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ E T -> StateT (TyState a) (Either (Err a)) ()
forall a. E T -> TyM a ()
checkAmb [E T
e, (Nm T, E T) -> E T
forall a b. (a, b) -> b
snd (Nm T, E T)
bs]
checkAmb (Lam T
_ Nm T
_ E T
e) = E T -> StateT (TyState a) (Either (Err a)) ()
forall a. E T -> TyM a ()
checkAmb E T
e
checkAmb e :: E T
e@(ParseAllCol T
t) | T -> Bool
isAmbiguous T
t = Err a -> StateT (TyState a) (Either (Err a)) ()
forall a. Err a -> StateT (TyState a) (Either (Err a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (T -> E () -> Err a
forall a. T -> E () -> Err a
Ambiguous T
t (E T -> E ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void E T
e))
checkAmb e :: E T
e@(ParseCol T
t Int
_) | T -> Bool
isAmbiguous T
t = Err a -> StateT (TyState a) (Either (Err a)) ()
forall a. Err a -> StateT (TyState a) (Either (Err a)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (T -> E () -> Err a
forall a. T -> E () -> Err a
Ambiguous T
t (E T -> E ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void E T
e))
checkAmb E T
_ = () -> StateT (TyState a) (Either (Err a)) ()
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

tS :: (t -> t -> f (a, t)) -> t -> [t] -> f ([a], t)
tS t -> t -> f (a, t)
_ t
s []     = ([a], t) -> f ([a], t)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], t
s)
tS t -> t -> f (a, t)
f t
s (t
t:[t]
ts) = do {(x, next) <- t -> t -> f (a, t)
f t
s t
t; first (x:) <$> tS f next ts}

tyP :: Ord a => Program a -> TyM a (Program T)
tyP :: forall a. Ord a => Program a -> TyM a (Program T)
tyP (Program [D a]
ds E a
e) = do
    (ds', s0) <- (IntMap T
 -> D a -> StateT (TyState a) (Either (Err a)) (D T, IntMap T))
-> IntMap T
-> [D a]
-> StateT (TyState a) (Either (Err a)) ([D T], IntMap T)
forall {f :: * -> *} {t} {t} {a}.
Monad f =>
(t -> t -> f (a, t)) -> t -> [t] -> f ([a], t)
tS IntMap T
-> D a -> StateT (TyState a) (Either (Err a)) (D T, IntMap T)
forall a. Ord a => IntMap T -> D a -> TyM a (D T, IntMap T)
tyDS IntMap T
forall a. Monoid a => a
mempty [D a]
ds
    (e', s1) <- tyES s0 e
    toCheck <- gets (IM.toList . classVars)
    traverse_ (uncurry (checkClass s1)) toCheck
    let res = {-# SCC "aT" #-} (T -> T) -> Program T -> Program T
forall a b. (a -> b) -> Program a -> Program b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (IntMap T -> T -> T
aT IntMap T
s1) ([D T] -> E T -> Program T
forall a. [D a] -> E a -> Program a
Program [D T]
ds' E T
e')
    checkAmb (expr res) $> res

tyNumOp :: Ord a => a -> TyM a T
tyNumOp :: forall a. Ord a => a -> TyM a T
tyNumOp a
l = do
    m <- Text -> TyM a (TyName ())
forall a. Text -> TyM a (TyName ())
freshN Text
"m"
    addCM m (IsNum, l)
    let m' = TyName () -> T
var TyName ()
m
    pure $ m' ~> m' ~> m'

tySemiOp :: Ord a => a -> TyM a T
tySemiOp :: forall a. Ord a => a -> TyM a T
tySemiOp a
l = do
    m <- Text -> TyM a (TyName ())
forall a. Text -> TyM a (TyName ())
freshN Text
"m"
    addCM m (IsSemigroup, l)
    let m' = TyName () -> T
var TyName ()
m
    pure $ m' ~> m' ~> m'

tyOrd :: Ord a => a -> TyM a T
tyOrd :: forall a. Ord a => a -> TyM a T
tyOrd a
l = do
    a <- Text -> TyM a (TyName ())
forall a. Text -> TyM a (TyName ())
freshN Text
"a"
    addCM a (IsOrd, l)
    let a' = TyName () -> T
var TyName ()
a
    pure $ a' ~> a' ~> tyB

tyEq :: Ord a => a -> TyM a T
tyEq :: forall a. Ord a => a -> TyM a T
tyEq a
l = do
    a <- Text -> TyM a (TyName ())
forall a. Text -> TyM a (TyName ())
freshN Text
"a"
    addCM a (IsEq, l)
    let a' = TyName () -> T
var TyName ()
a
    pure $ a' ~> a' ~> tyB

-- min/max
tyM :: Ord a => a -> TyM a T
tyM :: forall a. Ord a => a -> TyM a T
tyM a
l = do
    a <- Text -> TyM a (TyName ())
forall a. Text -> TyM a (TyName ())
freshN Text
"a"
    addCM a (IsOrd, l)
    let a' = TyName () -> T
var TyName ()
a
    pure $ a' ~> a' ~> a'

desugar :: a
desugar :: forall a. a
desugar = String -> a
forall a. (?callStack::CallStack) => String -> a
error String
"Internal error: should have been de-sugared in an earlier stage!"

tyE :: Ord a => E a -> TyM a (E T)
tyE :: forall a. Ord a => E a -> TyM a (E T)
tyE E a
e = do
    (e', s) <- IntMap T -> E a -> TyM a (E T, IntMap T)
forall a. Ord a => IntMap T -> E a -> TyM a (E T, IntMap T)
tyES IntMap T
forall a. Monoid a => a
mempty E a
e
    cvs <- gets (IM.toList . classVars)
    traverse_ (uncurry (checkClass s)) cvs
    pure (fmap (aT s) e')

tyES :: Ord a => Subst -> E a -> TyM a (E T, Subst)
tyES :: forall a. Ord a => IntMap T -> E a -> TyM a (E T, IntMap T)
tyES IntMap T
_ F{}                = String -> TyM a (E T, IntMap T)
forall a. (?callStack::CallStack) => String -> a
error String
"impossible."
tyES IntMap T
s (Lit a
_ (BLit Bool
b))   = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> L -> E T
forall a. a -> L -> E a
Lit T
tyB (Bool -> L
BLit Bool
b), IntMap T
s)
tyES IntMap T
s (Lit a
_ (ILit Integer
i))   = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> L -> E T
forall a. a -> L -> E a
Lit T
tyI (Integer -> L
ILit Integer
i), IntMap T
s)
tyES IntMap T
s (Lit a
_ (FLit Double
f))   = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> L -> E T
forall a. a -> L -> E a
Lit T
tyF (Double -> L
FLit Double
f), IntMap T
s)
tyES IntMap T
s (Lit a
_ (StrLit ByteString
str)) = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> L -> E T
forall a. a -> L -> E a
Lit T
tyStr (ByteString -> L
StrLit ByteString
str), IntMap T
s)
tyES IntMap T
s (RegexLit a
_ ByteString
rr)    = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> ByteString -> E T
forall a. a -> ByteString -> E a
RegexLit T
tyR ByteString
rr, IntMap T
s)
tyES IntMap T
s (Column a
_ Int
i)       = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> Int -> E T
forall a. a -> Int -> E a
Column (T -> T
tyStream T
tyStr) Int
i, IntMap T
s)
tyES IntMap T
s (IParseCol a
_ Int
i)    = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> Int -> E T
forall a. a -> Int -> E a
IParseCol (T -> T
tyStream T
tyI) Int
i, IntMap T
s)
tyES IntMap T
s (FParseCol a
_ Int
i)    = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> Int -> E T
forall a. a -> Int -> E a
FParseCol (T -> T
tyStream T
tyF) Int
i, IntMap T
s)
tyES IntMap T
s (Field a
_ Int
i)        = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> Int -> E T
forall a. a -> Int -> E a
Field T
tyStr Int
i, IntMap T
s)
tyES IntMap T
s LastField{}        = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> E T
forall a. a -> E a
LastField T
tyStr, IntMap T
s)
tyES IntMap T
s AllField{}         = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> E T
forall a. a -> E a
AllField T
tyStr, IntMap T
s)
tyES IntMap T
s FieldList{}        = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> E T
forall a. a -> E a
FieldList (T -> T
tyV T
tyStr), IntMap T
s)
tyES IntMap T
s AllColumn{}        = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> E T
forall a. a -> E a
AllColumn (T -> T
tyStream T
tyStr), IntMap T
s)
tyES IntMap T
s FParseAllCol{}     = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> E T
forall a. a -> E a
FParseAllCol (T -> T
tyStream T
tyF), IntMap T
s)
tyES IntMap T
s IParseAllCol{}     = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> E T
forall a. a -> E a
IParseAllCol (T -> T
tyStream T
tyI), IntMap T
s)
tyES IntMap T
s (ParseAllCol a
l)    = do {a <- Text -> TyM a (TyName ())
forall a. Text -> TyM a (TyName ())
freshN Text
"a"; addCM a (IsParse, l); pure (ParseAllCol (tyStream (var a)), s)}
tyES IntMap T
s (NB a
l N
MZ)    = do {m <- Text -> TyM a (TyName ())
forall a. Text -> TyM a (TyName ())
freshN Text
"m"; addCM m (IsMonoid, l); pure (NB (var m) MZ, s)}
tyES IntMap T
s (NB a
_ N
Ix)    = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> N -> E T
forall a. a -> N -> E a
NB T
tyI N
Ix, IntMap T
s)
tyES IntMap T
s (NB a
_ N
Fp)    = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> N -> E T
forall a. a -> N -> E a
NB T
tyStr N
Fp, IntMap T
s)
tyES IntMap T
s (NB a
_ N
Nf)    = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> N -> E T
forall a. a -> N -> E a
NB T
tyI N
Nf, IntMap T
s)
tyES IntMap T
s (BB a
l BBin
Plus)  = do {t <- a -> TyM a T
forall a. Ord a => a -> TyM a T
tySemiOp a
l; pure (BB t Plus, s)}
tyES IntMap T
s (BB a
l BBin
Minus) = do {t <- a -> TyM a T
forall a. Ord a => a -> TyM a T
tyNumOp a
l; pure (BB t Minus, s)}
tyES IntMap T
s (BB a
l BBin
Times) = do {t <- a -> TyM a T
forall a. Ord a => a -> TyM a T
tyNumOp a
l; pure (BB t Times, s)}
tyES IntMap T
s (BB a
l BBin
Exp)   = do {t <- a -> TyM a T
forall a. Ord a => a -> TyM a T
tyNumOp a
l; pure (BB t Exp, s)}
tyES IntMap T
s (BB a
l BBin
Gt)    = do {t <- a -> TyM a T
forall a. Ord a => a -> TyM a T
tyOrd a
l; pure (BB t Gt, s)}
tyES IntMap T
s (BB a
l BBin
Lt)    = do {t <- a -> TyM a T
forall a. Ord a => a -> TyM a T
tyOrd a
l; pure (BB t Lt, s)}
tyES IntMap T
s (BB a
l BBin
Geq)   = do {t <- a -> TyM a T
forall a. Ord a => a -> TyM a T
tyOrd a
l; pure (BB t Geq, s)}
tyES IntMap T
s (BB a
l BBin
Leq)   = do {t <- a -> TyM a T
forall a. Ord a => a -> TyM a T
tyOrd a
l; pure (BB t Leq, s)}
tyES IntMap T
s (BB a
l BBin
Eq)    = do {t <- a -> TyM a T
forall a. Ord a => a -> TyM a T
tyEq a
l; pure (BB t Eq, s)}
tyES IntMap T
s (BB a
l BBin
Neq)   = do {t <- a -> TyM a T
forall a. Ord a => a -> TyM a T
tyEq a
l; pure (BB t Neq, s)}
tyES IntMap T
s (BB a
l BBin
Min)   = do {t <- a -> TyM a T
forall a. Ord a => a -> TyM a T
tyM a
l; pure (BB t Min, s)}
tyES IntMap T
s (BB a
l BBin
Max)   = do {t <- a -> TyM a T
forall a. Ord a => a -> TyM a T
tyM a
l; pure (BB t Max, s)}
tyES IntMap T
s (BB a
_ BBin
Split) = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> BBin -> E T
forall a. a -> BBin -> E a
BB (T
tyStr T -> T -> T
~> T
tyR T -> T -> T
~> T -> T
tyV T
tyStr) BBin
Split, IntMap T
s)
tyES IntMap T
s (BB a
_ BBin
Splitc) = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> BBin -> E T
forall a. a -> BBin -> E a
BB (T
tyStr T -> T -> T
~> T
tyStr T -> T -> T
~> T -> T
tyV T
tyStr) BBin
Splitc, IntMap T
s)
tyES IntMap T
s (BB a
_ BBin
Matches) = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> BBin -> E T
forall a. a -> BBin -> E a
BB (T
tyStr T -> T -> T
~> T
tyR T -> T -> T
~> T
tyB) BBin
Matches, IntMap T
s)
tyES IntMap T
s (BB a
_ BBin
NotMatches) = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> BBin -> E T
forall a. a -> BBin -> E a
BB (T
tyStr T -> T -> T
~> T
tyR T -> T -> T
~> T
tyB) BBin
NotMatches, IntMap T
s)
tyES IntMap T
s (BB a
_ BBin
MMatch) = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> BBin -> E T
forall a. a -> BBin -> E a
BB (T
tyStr T -> T -> T
~> T
tyR T -> T -> T
~> T -> T
tyOpt T
tyStr) BBin
MMatch, IntMap T
s)
tyES IntMap T
s (UB a
_ BUn
Tally) = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> BUn -> E T
forall a. a -> BUn -> E a
UB (T
tyStr T -> T -> T
~> T
tyI) BUn
Tally, IntMap T
s)
tyES IntMap T
s (BB a
_ BBin
Take) = do {a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"; pure (BB (tyI ~> tyV a ~> tyV a) Take, s)}
tyES IntMap T
s (BB a
_ BBin
Drop) = do {a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"; pure (BB (tyI ~> tyV a ~> tyV a) Drop, s)}
tyES IntMap T
s (BB a
_ BBin
Div) = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> BBin -> E T
forall a. a -> BBin -> E a
BB (T
tyF T -> T -> T
~> T
tyF T -> T -> T
~> T
tyF) BBin
Div, IntMap T
s)
tyES IntMap T
s (UB a
_ BUn
Not) = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> BUn -> E T
forall a. a -> BUn -> E a
UB (T
tyB T -> T -> T
~> T
tyB) BUn
Not, IntMap T
s)
tyES IntMap T
s (BB a
_ BBin
And) = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> BBin -> E T
forall a. a -> BBin -> E a
BB (T
tyB T -> T -> T
~> T
tyB T -> T -> T
~> T
tyB) BBin
And, IntMap T
s)
tyES IntMap T
s (BB a
_ BBin
Or) = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> BBin -> E T
forall a. a -> BBin -> E a
BB (T
tyB T -> T -> T
~> T
tyB T -> T -> T
~> T
tyB) BBin
Or, IntMap T
s)
tyES IntMap T
s (BB a
_ BBin
Match) = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> BBin -> E T
forall a. a -> BBin -> E a
BB (T
tyStr T -> T -> T
~> T
tyR T -> T -> T
~> T -> T
tyOpt ([T] -> T
TyTup [T
tyI, T
tyI])) BBin
Match, IntMap T
s)
tyES IntMap T
s (TB a
_ BTer
Substr) = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> BTer -> E T
forall a. a -> BTer -> E a
TB (T
tyStr T -> T -> T
~> T
tyI T -> T -> T
~> T
tyI T -> T -> T
~> T
tyStr) BTer
Substr, IntMap T
s)
tyES IntMap T
s (TB a
_ BTer
Sub1) = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> BTer -> E T
forall a. a -> BTer -> E a
TB (T
tyR T -> T -> T
~> T
tyStr T -> T -> T
~> T
tyStr T -> T -> T
~> T
tyStr) BTer
Sub1, IntMap T
s)
tyES IntMap T
s (TB a
_ BTer
Subs) = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> BTer -> E T
forall a. a -> BTer -> E a
TB (T
tyR T -> T -> T
~> T
tyStr T -> T -> T
~> T
tyStr T -> T -> T
~> T
tyStr) BTer
Subs, IntMap T
s)
tyES IntMap T
s (UB a
_ BUn
IParse) = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> BUn -> E T
forall a. a -> BUn -> E a
UB (T
tyStr T -> T -> T
~> T
tyI) BUn
IParse, IntMap T
s)
tyES IntMap T
s (UB a
_ BUn
FParse) = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> BUn -> E T
forall a. a -> BUn -> E a
UB (T -> T -> T
tyArr T
tyStr T
tyF) BUn
FParse, IntMap T
s)
tyES IntMap T
s (UB a
_ BUn
Floor) = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> BUn -> E T
forall a. a -> BUn -> E a
UB (T -> T -> T
tyArr T
tyF T
tyI) BUn
Floor, IntMap T
s)
tyES IntMap T
s (UB a
_ BUn
Ceiling) = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> BUn -> E T
forall a. a -> BUn -> E a
UB (T
tyF T -> T -> T
~> T
tyI) BUn
Ceiling, IntMap T
s)
tyES IntMap T
s (UB a
_ BUn
Head) = do {a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"; pure (UB (tyV a ~> a) Head, s)}
tyES IntMap T
s (UB a
_ BUn
Tail) = do {a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"; pure (UB (tyV a ~> tyV a) Tail, s)}
tyES IntMap T
s (UB a
_ BUn
Last) = do {a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"; pure (UB (tyV a ~> a) Last, s)}
tyES IntMap T
s (UB a
_ BUn
Init) = do {a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"; pure (UB (tyV a ~> tyV a) Init, s)}
tyES IntMap T
s (BB a
_ BBin
Report) = do {a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"; b <- freshTV "b"; pure (BB (tyStream a ~> b ~> TyB TyUnit) Report, s)}
tyES IntMap T
s (UB a
_ BUn
TallyList) = do {a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"; pure (UB (a ~> tyI) TallyList, s)}
tyES IntMap T
s (UB a
l BUn
Negate) = do {a <- Text -> TyM a (TyName ())
forall a. Text -> TyM a (TyName ())
freshN Text
"a"; addCM a (IsNum, l); let a'=TyName () -> T
var TyName ()
a in pure (UB (tyArr a' a') Negate, s)}
tyES IntMap T
s (UB a
_ BUn
Some) = do {a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"; pure (UB (tyArr a (tyOpt a)) Some, s)}
tyES IntMap T
s (NB a
_ N
None) = do {a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"; pure (NB (tyOpt a) None, s)}
tyES IntMap T
s (ParseCol a
l Int
i) = do {a <- Text -> TyM a (TyName ())
forall a. Text -> TyM a (TyName ())
freshN Text
"a"; addCM a (IsParse, l); pure (ParseCol (tyStream (var a)) i, s)}
tyES IntMap T
s (UB a
l BUn
Parse) = do {a <- Text -> TyM a (TyName ())
forall a. Text -> TyM a (TyName ())
freshN Text
"a"; addCM a (IsParse, l); pure (UB (tyStr ~> var a) Parse, s)}
tyES IntMap T
s (BB a
l BBin
Sprintf) = do {a <- Text -> TyM a (TyName ())
forall a. Text -> TyM a (TyName ())
freshN Text
"a"; addCM a (IsPrintf, l); pure (BB (tyStr ~> var a ~> tyStr) Sprintf, s)}
tyES IntMap T
s (BB a
l BBin
Rein) = do {f <- Text -> TyM a (TyName ())
forall a. Text -> TyM a (TyName ())
freshN Text
"f"; addCM f (Foldable, l); pure (BB (tyStr ~> (var f:$tyStr) ~> tyStr) Rein, s)}
tyES IntMap T
s (BB a
l BBin
Nier) = do {f <- Text -> TyM a (TyName ())
forall a. Text -> TyM a (TyName ())
freshN Text
"f"; addCM f (Foldable, l); pure (BB ((var f:$tyStr) ~> tyStr ~> tyStr) Nier, s)}
tyES IntMap T
s (BB a
l BBin
DedupOn) = do {a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"; b <- freshN "b"; addCM b (IsEq, l); let b'=TyName () -> T
var TyName ()
b in pure (BB (tyArr (a ~> b') (tyArr (tyStream a) (tyStream b'))) DedupOn, s)}
tyES IntMap T
s (UB a
_ (At Int
i)) = do {a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"; pure (UB (tyV a ~> a) (At i), s)}
tyES IntMap T
s (UB a
l BUn
Dedup) = do {a <- Text -> TyM a (TyName ())
forall a. Text -> TyM a (TyName ())
freshN Text
"a"; addCM a (IsEq, l); let sA=T -> T
tyStream (TyName () -> T
var TyName ()
a) in pure (UB (sA ~> sA) Dedup, s)}
tyES IntMap T
s (UB a
_ BUn
Const) = do {a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"; b <- freshTV "b"; pure (UB (a ~> b ~> a) Const, s)}
tyES IntMap T
s (UB a
l BUn
CatMaybes) = do {a <- Text -> TyM a (TyName ())
forall a. Text -> TyM a (TyName ())
freshN Text
"a"; f <- freshN "f"; addCM f (Witherable, l); let a'=TyName () -> T
var TyName ()
a; f'=TyName () -> T
var TyName ()
f in pure (UB (tyArr (f':$tyOpt a') (f':$a')) CatMaybes, s)}
tyES IntMap T
s (BB a
l BBin
Filter) = do {a <- Text -> TyM a (TyName ())
forall a. Text -> TyM a (TyName ())
freshN Text
"a"; f <- freshN "f"; addCM f (Witherable, l); let a'=TyName () -> T
var TyName ()
a; f'=TyName () -> T
var TyName ()
f; w=T
f'T -> T -> T
:$T
a' in pure (BB ((a' ~> tyB) ~> w ~> w) Filter, s)}
tyES IntMap T
s (UB a
_ (Select Int
i)) = do
    ρ <- Text -> TyM a (TyName ())
forall a. Text -> TyM a (TyName ())
freshN Text
"ρ"; a <- freshTV "a"
    pure (UB (Rho ρ (IM.singleton i a) ~> a) (Select i), s)
tyES IntMap T
s (UB a
_ (SelR TyName ()
n)) = do
    ρ <- Text -> TyM a (TyName ())
forall a. Text -> TyM a (TyName ())
freshN Text
"ρ"; a <- freshTV "a"
    pure (UB (Ρ ρ (Nm.singleton n a) ~> a) (SelR n), s)
tyES IntMap T
s (BB a
l BBin
MapMaybe) = do
    a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"; b <- freshTV "b"
    f <- freshN "f"
    addCM f (Witherable, l)
    let f'=TyName () -> T
var TyName ()
f
    pure (BB (tyArr (a ~> tyOpt b) ((f':$a) ~> (f':$b))) MapMaybe, s)
tyES IntMap T
s (BB a
l BBin
Map) = do
    a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"; b <- freshTV "b"
    f <- freshN "f"
    let f'=TyName () -> T
var TyName ()
f
    addCM f (Functor, l)
    pure (BB (tyArr (a ~> b) ((f':$a) ~> (f':$b))) Map, s)
tyES IntMap T
s (TB a
l BTer
Fold) = do
    a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"; b <- freshTV "b"
    f <- freshN "f"
    let f'=TyName () -> T
var TyName ()
f
    addCM f (Foldable, l)
    pure (TB ((b ~> a ~> b) ~> (b ~> (f':$a) ~> b)) Fold, s)
tyES IntMap T
s (BB a
l BBin
Fold1) = do
    a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"
    f <- freshN "f"
    let f'=TyName () -> T
var TyName ()
f
    addCM f (Foldable, l)
    pure (BB ((a ~> a ~> a) ~> ((f':$a) ~> a)) Fold1, s)
tyES IntMap T
s (TB a
_ BTer
Bookend) = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> BTer -> E T
forall a. a -> BTer -> E a
TB (T
tyR T -> T -> T
~> T
tyR T -> T -> T
~> T -> T
tyStream T
tyStr T -> T -> T
~> T -> T
tyStream T
tyStr) BTer
Bookend, IntMap T
s)
tyES IntMap T
s (TB a
_ BTer
Captures) = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> BTer -> E T
forall a. a -> BTer -> E a
TB (T
tyStr T -> T -> T
~> T
tyI T -> T -> T
~> T
tyR T -> T -> T
~> T -> T
tyOpt T
tyStr) BTer
Captures, IntMap T
s)
tyES IntMap T
s (BB a
_ BBin
Prior) = do
    a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"; b <- freshTV "b"
    pure (BB (tyArr (a ~> a ~> b) (tyStream a ~> tyStream b)) Prior, s)
tyES IntMap T
s (TB a
_ BTer
ZipW) = do
    a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"; b <- freshTV "b"; c <- freshTV "c"
    pure (TB (tyArr (a ~> b ~> c) (tyStream a ~> tyStream b ~> tyStream c)) ZipW, s)
tyES IntMap T
s (TB a
_ BTer
Scan) = do
    a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"; b <- freshTV "b"
    pure (TB (tyArr (b ~> a ~> b) (b ~> tyStream a ~> tyStream b)) Scan, s)
tyES IntMap T
s (TB a
_ BTer
ScanList) = do
    a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"; b <- freshTV "b"
    pure (TB (tyArr (b ~> a ~> b) (b ~> tyV a ~> tyV b)) ScanList, s)
tyES IntMap T
s (TB a
_ BTer
Option) = do
    a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"; b <- freshTV "b"
    pure (TB (b ~> (a ~> b) ~> tyOpt a ~> b) Option, s)
tyES IntMap T
s (TB a
_ BTer
Ixes) = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> BTer -> E T
forall a. a -> BTer -> E a
TB (T
tyStr T -> T -> T
~> T
tyI T -> T -> T
~> T
tyR T -> T -> T
~> T -> T
tyV ([T] -> T
TyTup [T
tyI, T
tyI])) BTer
Ixes, IntMap T
s)
tyES IntMap T
s (TB a
_ BTer
AllCaptures) = (E T, IntMap T) -> TyM a (E T, IntMap T)
forall a. a -> StateT (TyState a) (Either (Err a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (T -> BTer -> E T
forall a. a -> BTer -> E a
TB (T
tyStr T -> T -> T
~> T
tyI T -> T -> T
~> T
tyR T -> T -> T
~> T -> T
tyV T
tyStr) BTer
AllCaptures, IntMap T
s)
tyES IntMap T
s (Implicit a
_ E a
e) = do {(e',s') <- IntMap T -> E a -> TyM a (E T, IntMap T)
forall a. Ord a => IntMap T -> E a -> TyM a (E T, IntMap T)
tyES IntMap T
s E a
e; pure (Implicit (tyStream (eLoc e')) e', s')}
tyES IntMap T
s (Guarded a
l E a
e E a
se) = do
    (se', s0) <- IntMap T -> E a -> TyM a (E T, IntMap T)
forall a. Ord a => IntMap T -> E a -> TyM a (E T, IntMap T)
tyES IntMap T
s E a
se
    (e', s1) <- tyES s0 e
    s2 <- liftEither $ mguPrep l s1 tyB (eLoc e')
    pure (Guarded (tyStream (eLoc se')) e' se', s2)
tyES IntMap T
s (EApp a
l E a
e0 E a
e1)     = do
    a <- Text -> TyM a (TyName ())
forall a. Text -> TyM a (TyName ())
freshN Text
"a"; b <- freshN "b"
    let a'=TyName () -> T
var TyName ()
a; b'=TyName () -> T
var TyName ()
b; e0Ty=T
a' T -> T -> T
~> T
b'
    (e0', s0) <- tyES s e0
    (e1', s1) <- tyES s0 e1
    s2 <- liftEither $ mguPrep l s1 (eLoc e0') e0Ty
    s3 <- liftEither $ mguPrep l s2 (eLoc e1') a'
    pure (EApp b' e0' e1', s3)
tyES IntMap T
s (Lam a
_ n :: Nm a
n@(Nm Text
_ (U Int
i) a
_) E a
e) = do
    a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"
    addVarM i a
    (e', s') <- tyES s e
    pure (Lam (a ~> eLoc e') (n$>a) e', s')
tyES IntMap T
s (Let a
_ (n :: Nm a
n@(Nm Text
_ (U Int
i) a
_), E a
eϵ) E a
e) = do
    (eϵ', s0) <- IntMap T -> E a -> TyM a (E T, IntMap T)
forall a. Ord a => IntMap T -> E a -> TyM a (E T, IntMap T)
tyES IntMap T
s E a
eϵ
    let bTy=E T -> T
forall a. E a -> a
eLoc E T
eϵ'
    addVarM i bTy
    (e', s1) <- tyES s0 e
    pure (Let (eLoc e') (n$>bTy, eϵ') e', s1)
tyES IntMap T
s (Tup a
_ [E a]
es) = do {(es', s') <- (IntMap T -> E a -> TyM a (E T, IntMap T))
-> IntMap T
-> [E a]
-> StateT (TyState a) (Either (Err a)) ([E T], IntMap T)
forall {f :: * -> *} {t} {t} {a}.
Monad f =>
(t -> t -> f (a, t)) -> t -> [t] -> f ([a], t)
tS IntMap T -> E a -> TyM a (E T, IntMap T)
forall a. Ord a => IntMap T -> E a -> TyM a (E T, IntMap T)
tyES IntMap T
s [E a]
es; pure (Tup (TyTup (fmap eLoc es')) es', s')}
tyES IntMap T
s (Rec a
_ [(Nm a, E a)]
es) = do
    (es', s') <- (IntMap T -> E a -> TyM a (E T, IntMap T))
-> IntMap T
-> [E a]
-> StateT (TyState a) (Either (Err a)) ([E T], IntMap T)
forall {f :: * -> *} {t} {t} {a}.
Monad f =>
(t -> t -> f (a, t)) -> t -> [t] -> f ([a], t)
tS IntMap T -> E a -> TyM a (E T, IntMap T)
forall a. Ord a => IntMap T -> E a -> TyM a (E T, IntMap T)
tyES IntMap T
s [E a]
esϵ
    let ts=E T -> T
forall a. E a -> a
eLoc(E T -> T) -> [E T] -> [T]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>[E T]
es'; ns'=(Nm a -> T -> Nm T) -> [Nm a] -> [T] -> [Nm T]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Nm a -> T -> Nm T
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
($>) [Nm a]
ns [T]
ts
    pure (Rec (TyRec (Nm.fromList (zip (void<$>ns) ts))) (zip ns' es'), s')
  where
    ([Nm a]
ns,[E a]
esϵ) = [(Nm a, E a)] -> ([Nm a], [E a])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Nm a, E a)]
es
tyES IntMap T
s (Var a
_ Nm a
n) = do {t <- Nm a -> TyM a T
forall a. Nm a -> TyM a T
lookupVar Nm a
n; pure (Var t (n$>t), s)}
tyES IntMap T
s (OptionVal a
_ (Just E a
e)) = do {(e', s') <- IntMap T -> E a -> TyM a (E T, IntMap T)
forall a. Ord a => IntMap T -> E a -> TyM a (E T, IntMap T)
tyES IntMap T
s E a
e; pure (OptionVal (tyOpt (eLoc e')) (Just e'), s')}
tyES IntMap T
s (OptionVal a
_ Maybe (E a)
Nothing) = do {a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"; pure (OptionVal (tyOpt a) Nothing, s)}
tyES IntMap T
s (Arr a
l Vector (E a)
v) | Vector (E a) -> Bool
forall a. Vector a -> Bool
V.null Vector (E a)
v = do
    a <- Text -> TyM a T
forall a. Text -> TyM a T
freshTV Text
"a"
    pure (Arr (tyV a) V.empty, s)
                 | Bool
otherwise = do
    (v',s0) <- (IntMap T -> E a -> TyM a (E T, IntMap T))
-> IntMap T
-> [E a]
-> StateT (TyState a) (Either (Err a)) ([E T], IntMap T)
forall {f :: * -> *} {t} {t} {a}.
Monad f =>
(t -> t -> f (a, t)) -> t -> [t] -> f ([a], t)
tS IntMap T -> E a -> TyM a (E T, IntMap T)
forall a. Ord a => IntMap T -> E a -> TyM a (E T, IntMap T)
tyES IntMap T
s (Vector (E a) -> [E a]
forall a. Vector a -> [a]
V.toList Vector (E a)
v)
    let vt=(E T -> T) -> [E T] -> [T]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap E T -> T
forall a. E a -> a
eLoc [E T]
v'
    s1 <- liftEither $ zS (mguPrep l) s0 vt (tail vt)
    pure (Arr (head vt) (V.fromList v'), s1)
tyES IntMap T
s (Cond a
l E a
p E a
e0 E a
e1) = do
    (p', s0) <- IntMap T -> E a -> TyM a (E T, IntMap T)
forall a. Ord a => IntMap T -> E a -> TyM a (E T, IntMap T)
tyES IntMap T
s E a
p
    (e0', s1) <- tyES s0 e0
    (e1', s2) <- tyES s1 e1
    let t=E T -> T
forall a. E a -> a
eLoc E T
e0'
    s3 <- liftEither $ mguPrep l s2 tyB (eLoc p')
    s4 <- liftEither $ mguPrep l s3 t (eLoc e1')
    pure (Cond t p' e0' e1', s4)
tyES IntMap T
s (Anchor a
l [E a]
es) = do
    (es', s') <- (IntMap T -> E a -> TyM a (E T, IntMap T))
-> IntMap T
-> [E a]
-> StateT (TyState a) (Either (Err a)) ([E T], IntMap T)
forall {f :: * -> *} {t} {t} {a}.
Monad f =>
(t -> t -> f (a, t)) -> t -> [t] -> f ([a], t)
tS (\IntMap T
sϵ E a
e -> do {(e',s0) <- IntMap T -> E a -> TyM a (E T, IntMap T)
forall a. Ord a => IntMap T -> E a -> TyM a (E T, IntMap T)
tyES IntMap T
sϵ E a
e; a <- freshTV "a"; s1 <- liftEither $ mguPrep l s0 (tyStream a) (eLoc e'); pure (e', s1)}) IntMap T
s [E a]
es
    pure (Anchor (TyB TyUnit) es', s')
tyES IntMap T
_ RC{} = String -> TyM a (E T, IntMap T)
forall a. (?callStack::CallStack) => String -> a
error String
"Internal error: regex should not be compiled at this stage."
tyES IntMap T
_ Dfn{} = TyM a (E T, IntMap T)
forall a. a
desugar; tyES IntMap T
_ ResVar{} = TyM a (E T, IntMap T)
forall a. a
desugar; tyES IntMap T
_ Paren{} = TyM a (E T, IntMap T)
forall a. a
desugar; tyES IntMap T
_ RwB{} = TyM a (E T, IntMap T)
forall a. a
desugar; tyES IntMap T
_ RwT{} = TyM a (E T, IntMap T)
forall a. a
desugar