{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE InstanceSigs #-}

module Gibbon.L0.Typecheck where

import           Control.Monad.State ( MonadState )
import           Control.Monad.Except
#if !MIN_VERSION_base(4,13,0)
-- https://downloads.haskell.org/ghc/8.8.1/docs/html/users_guide/8.8.1-notes.html
import           Control.Monad.Fail(MonadFail(..))
#endif
import           Data.Foldable ( foldlM )
import qualified Data.List as L
import qualified Data.Map as M
import qualified Data.Set as S
import           Text.PrettyPrint hiding ( (<>) )
import           Text.PrettyPrint.GenericPretty
#if !MIN_VERSION_base(4,11,0)
import           Data.Semigroup
#endif

import           Gibbon.L0.Syntax as L0
import           Gibbon.Common
import           Data.Function
import           Data.Bitraversable

--------------------------------------------------------------------------------

newtype TcM a = TcM (ExceptT Doc PassM a)
  deriving ((forall a b. (a -> b) -> TcM a -> TcM b)
-> (forall a b. a -> TcM b -> TcM a) -> Functor TcM
forall a b. a -> TcM b -> TcM a
forall a b. (a -> b) -> TcM a -> TcM 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) -> TcM a -> TcM b
fmap :: forall a b. (a -> b) -> TcM a -> TcM b
$c<$ :: forall a b. a -> TcM b -> TcM a
<$ :: forall a b. a -> TcM b -> TcM a
Functor, Functor TcM
Functor TcM
-> (forall a. a -> TcM a)
-> (forall a b. TcM (a -> b) -> TcM a -> TcM b)
-> (forall a b c. (a -> b -> c) -> TcM a -> TcM b -> TcM c)
-> (forall a b. TcM a -> TcM b -> TcM b)
-> (forall a b. TcM a -> TcM b -> TcM a)
-> Applicative TcM
forall a. a -> TcM a
forall a b. TcM a -> TcM b -> TcM a
forall a b. TcM a -> TcM b -> TcM b
forall a b. TcM (a -> b) -> TcM a -> TcM b
forall a b c. (a -> b -> c) -> TcM a -> TcM b -> TcM c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall a. a -> TcM a
pure :: forall a. a -> TcM a
$c<*> :: forall a b. TcM (a -> b) -> TcM a -> TcM b
<*> :: forall a b. TcM (a -> b) -> TcM a -> TcM b
$cliftA2 :: forall a b c. (a -> b -> c) -> TcM a -> TcM b -> TcM c
liftA2 :: forall a b c. (a -> b -> c) -> TcM a -> TcM b -> TcM c
$c*> :: forall a b. TcM a -> TcM b -> TcM b
*> :: forall a b. TcM a -> TcM b -> TcM b
$c<* :: forall a b. TcM a -> TcM b -> TcM a
<* :: forall a b. TcM a -> TcM b -> TcM a
Applicative, Applicative TcM
Applicative TcM
-> (forall a b. TcM a -> (a -> TcM b) -> TcM b)
-> (forall a b. TcM a -> TcM b -> TcM b)
-> (forall a. a -> TcM a)
-> Monad TcM
forall a. a -> TcM a
forall a b. TcM a -> TcM b -> TcM b
forall a b. TcM a -> (a -> TcM b) -> TcM b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall a b. TcM a -> (a -> TcM b) -> TcM b
>>= :: forall a b. TcM a -> (a -> TcM b) -> TcM b
$c>> :: forall a b. TcM a -> TcM b -> TcM b
>> :: forall a b. TcM a -> TcM b -> TcM b
$creturn :: forall a. a -> TcM a
return :: forall a. a -> TcM a
Monad, MonadError Doc, MonadState Int)

instance MonadFail TcM where
  fail :: forall a. String -> TcM a
fail = String -> TcM a
forall a. HasCallStack => String -> a
error

runTcM :: TcM a -> PassM (Either Doc a)
runTcM :: forall a. TcM a -> PassM (Either Doc a)
runTcM (TcM ExceptT Doc PassM a
tc) = ExceptT Doc PassM a -> PassM (Either Doc a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT Doc PassM a
tc

err :: Doc -> TcM a
err :: forall a. Doc -> TcM a
err Doc
d = Doc -> TcM a
forall a. Doc -> TcM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Doc
"L0.Typecheck: " Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
4 Doc
d)

tcProg :: Prog0 -> PassM Prog0
tcProg :: Prog0 -> PassM Prog0
tcProg prg :: Prog0
prg@Prog{DDefs (TyOf Exp0)
ddefs :: DDefs (TyOf Exp0)
ddefs :: forall ex. Prog ex -> DDefs (TyOf ex)
ddefs,FunDefs Exp0
fundefs :: FunDefs Exp0
fundefs :: forall ex. Prog ex -> FunDefs ex
fundefs,Maybe (Exp0, TyOf Exp0)
mainExp :: Maybe (Exp0, TyOf Exp0)
mainExp :: forall ex. Prog ex -> Maybe (ex, TyOf ex)
mainExp} = do
  let init_fenv :: Map Var TyScheme
init_fenv = (FunDef Exp0 -> TyScheme) -> FunDefs Exp0 -> Map Var TyScheme
forall a b k. (a -> b) -> Map k a -> Map k b
M.map FunDef Exp0 -> ArrowTy (TyOf Exp0)
FunDef Exp0 -> TyScheme
forall ex. FunDef ex -> ArrowTy (TyOf ex)
funTy FunDefs Exp0
fundefs
  FunDefs Exp0
fundefs_tc <- (FunDef Exp0 -> PassM (FunDef Exp0))
-> FunDefs Exp0 -> PassM (FunDefs Exp0)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Map Var a -> m (Map Var b)
mapM (DDefs0 -> Map Var TyScheme -> FunDef Exp0 -> PassM (FunDef Exp0)
tcFun DDefs (TyOf Exp0)
DDefs0
ddefs Map Var TyScheme
init_fenv) FunDefs Exp0
fundefs
  -- generalize top level functions, e.g. `foo x = x :: $0 -> $0` to `foo x = x :: forall x. x -> x`
  FunDefs Exp0
fundefs' <-  (FunDef Exp0 -> PassM (FunDef Exp0))
-> FunDefs Exp0 -> PassM (FunDefs Exp0)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Map Var a -> m (Map Var b)
mapM (\FunDef Exp0
fndef -> do
                              TyScheme
fnty'' <- (Doc -> TyScheme)
-> (TyScheme -> TyScheme) -> Either Doc TyScheme -> TyScheme
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (String -> TyScheme
forall a. HasCallStack => String -> a
error (String -> TyScheme) -> (Doc -> String) -> Doc -> TyScheme
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
render) TyScheme -> TyScheme
forall a. a -> a
id (Either Doc TyScheme -> TyScheme)
-> PassM (Either Doc TyScheme) -> PassM TyScheme
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcM TyScheme -> PassM (Either Doc TyScheme)
forall a. TcM a -> PassM (Either Doc a)
runTcM ((Subst, TyScheme) -> TyScheme
forall a b. (a, b) -> b
snd ((Subst, TyScheme) -> TyScheme)
-> TcM (Subst, TyScheme) -> TcM TyScheme
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Var TyScheme
-> Subst -> [TyVar] -> Ty0 -> TcM (Subst, TyScheme)
generalize Map Var TyScheme
forall k a. Map k a
M.empty Subst
emptySubst [] (TyScheme -> Ty0
tyFromScheme (FunDef Exp0 -> ArrowTy (TyOf Exp0)
forall ex. FunDef ex -> ArrowTy (TyOf ex)
funTy FunDef Exp0
fndef)))
                              FunDef Exp0 -> PassM (FunDef Exp0)
forall a. a -> PassM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FunDef Exp0 -> PassM (FunDef Exp0))
-> FunDef Exp0 -> PassM (FunDef Exp0)
forall a b. (a -> b) -> a -> b
$ FunDef Exp0
fndef {funTy :: ArrowTy (TyOf Exp0)
funTy = ArrowTy (TyOf Exp0)
TyScheme
fnty''}
                           ) FunDefs Exp0
fundefs_tc
  let fenv :: Map Var TyScheme
fenv = (FunDef Exp0 -> TyScheme) -> FunDefs Exp0 -> Map Var TyScheme
forall a b k. (a -> b) -> Map k a -> Map k b
M.map FunDef Exp0 -> ArrowTy (TyOf Exp0)
FunDef Exp0 -> TyScheme
forall ex. FunDef ex -> ArrowTy (TyOf ex)
funTy FunDefs Exp0
fundefs'
  -- Run the typechecker on the expression, and update it's type in the program
  -- (the parser initializes the main expression with the void type).
  Maybe (Exp0, Ty0)
mainExp' <- case Maybe (Exp0, TyOf Exp0)
mainExp of
                Maybe (Exp0, TyOf Exp0)
Nothing -> Maybe (Exp0, Ty0) -> PassM (Maybe (Exp0, Ty0))
forall a. a -> PassM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Exp0, Ty0)
forall a. Maybe a
Nothing
                Just (Exp0
e,TyOf Exp0
gvn_main_ty) -> do
                  let tc :: TcM (Subst, Ty0, Exp0)
tc = do
                              (Subst
s1, Ty0
drvd_main_ty, Exp0
e_tc) <-
                                DDefs0
-> Subst
-> Map Var TyScheme
-> Map Var TyScheme
-> [TyVar]
-> Bool
-> Exp0
-> TcM (Subst, Ty0, Exp0)
tcExp DDefs (TyOf Exp0)
DDefs0
ddefs Subst
emptySubst Map Var TyScheme
forall k a. Map k a
M.empty Map Var TyScheme
fenv [] Bool
True Exp0
e
                              Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify Exp0
e TyOf Exp0
Ty0
gvn_main_ty Ty0
drvd_main_ty
                              -- let e_tc' = fixTyApps s1 e_tc
                              (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, Subst -> Ty0 -> Ty0
zonkTy Subst
s2 Ty0
drvd_main_ty, Exp0
e_tc)
                  Either Doc (Subst, Ty0, Exp0)
res <- TcM (Subst, Ty0, Exp0) -> PassM (Either Doc (Subst, Ty0, Exp0))
forall a. TcM a -> PassM (Either Doc a)
runTcM TcM (Subst, Ty0, Exp0)
tc
                  case Either Doc (Subst, Ty0, Exp0)
res of
                    Left Doc
er -> String -> PassM (Maybe (Exp0, Ty0))
forall a. HasCallStack => String -> a
error (Doc -> String
render Doc
er)
                    Right (Subst
_s, Ty0
ty, Exp0
e_tc) -> Maybe (Exp0, Ty0) -> PassM (Maybe (Exp0, Ty0))
forall a. a -> PassM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Exp0, Ty0) -> PassM (Maybe (Exp0, Ty0)))
-> Maybe (Exp0, Ty0) -> PassM (Maybe (Exp0, Ty0))
forall a b. (a -> b) -> a -> b
$ (Exp0, Ty0) -> Maybe (Exp0, Ty0)
forall a. a -> Maybe a
Just (Exp0
e_tc, Ty0
ty)
  Prog0 -> PassM Prog0
forall a. a -> PassM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Prog0
prg { fundefs :: FunDefs Exp0
fundefs = FunDefs Exp0
fundefs'
           , mainExp :: Maybe (Exp0, TyOf Exp0)
mainExp = Maybe (Exp0, TyOf Exp0)
Maybe (Exp0, Ty0)
mainExp' }

tcFun :: DDefs0 -> Gamma -> FunDef0 -> PassM FunDef0
tcFun :: DDefs0 -> Map Var TyScheme -> FunDef Exp0 -> PassM (FunDef Exp0)
tcFun DDefs0
ddefs Map Var TyScheme
fenv fn :: FunDef Exp0
fn@FunDef{[Var]
funArgs :: [Var]
funArgs :: forall ex. FunDef ex -> [Var]
funArgs,ArrowTy (TyOf Exp0)
funTy :: forall ex. FunDef ex -> ArrowTy (TyOf ex)
funTy :: ArrowTy (TyOf Exp0)
funTy,Exp0
funBody :: Exp0
funBody :: forall ex. FunDef ex -> ex
funBody, Var
funName :: Var
funName :: forall ex. FunDef ex -> Var
funName} = do
  Either Doc (FunDef Exp0)
res <- TcM (FunDef Exp0) -> PassM (Either Doc (FunDef Exp0))
forall a. TcM a -> PassM (Either Doc a)
runTcM (TcM (FunDef Exp0) -> PassM (Either Doc (FunDef Exp0)))
-> TcM (FunDef Exp0) -> PassM (Either Doc (FunDef Exp0))
forall a b. (a -> b) -> a -> b
$ do
    let (ForAll [TyVar]
tyvars (ArrowTy [Ty0]
gvn_arg_tys Ty0
gvn_retty)) = ArrowTy (TyOf Exp0)
funTy
        init_venv :: Map Var TyScheme
init_venv = [(Var, TyScheme)] -> Map Var TyScheme
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Var, TyScheme)] -> Map Var TyScheme)
-> [(Var, TyScheme)] -> Map Var TyScheme
forall a b. (a -> b) -> a -> b
$ [Var] -> [TyScheme] -> [(Var, TyScheme)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
funArgs ([TyScheme] -> [(Var, TyScheme)])
-> [TyScheme] -> [(Var, TyScheme)]
forall a b. (a -> b) -> a -> b
$ (Ty0 -> TyScheme) -> [Ty0] -> [TyScheme]
forall a b. (a -> b) -> [a] -> [b]
map ([TyVar] -> Ty0 -> TyScheme
ForAll []) [Ty0]
gvn_arg_tys
        init_s :: Subst
init_s = Subst
emptySubst
    (Subst
s1, Ty0
drvd_funBody_ty, Exp0
funBody_tc) <-
      DDefs0
-> Subst
-> Map Var TyScheme
-> Map Var TyScheme
-> [TyVar]
-> Bool
-> Exp0
-> TcM (Subst, Ty0, Exp0)
tcExp DDefs0
ddefs Subst
init_s Map Var TyScheme
init_venv Map Var TyScheme
fenv [TyVar]
tyvars Bool
False Exp0
funBody
    Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify Exp0
funBody Ty0
drvd_funBody_ty Ty0
gvn_retty
    FunDef Exp0 -> TcM (FunDef Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FunDef Exp0 -> TcM (FunDef Exp0))
-> FunDef Exp0 -> TcM (FunDef Exp0)
forall a b. (a -> b) -> a -> b
$ FunDef Exp0
fn { funTy :: ArrowTy (TyOf Exp0)
funTy   = Subst -> TyScheme -> TyScheme
zonkTyScheme (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2) ArrowTy (TyOf Exp0)
TyScheme
funTy
              , funBody :: Exp0
funBody = Subst -> Exp0 -> Exp0
zonkExp (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2) Exp0
funBody_tc }
  case Either Doc (FunDef Exp0)
res of
    Left Doc
er   -> String -> PassM (FunDef Exp0)
forall a. HasCallStack => String -> a
error (String -> PassM (FunDef Exp0)) -> String -> PassM (FunDef Exp0)
forall a b. (a -> b) -> a -> b
$ Doc -> String
render Doc
er String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Var -> String
forall a. Show a => a -> String
show Var
funName
    Right FunDef Exp0
fn1 -> FunDef Exp0 -> PassM (FunDef Exp0)
forall a. a -> PassM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FunDef Exp0
fn1

tcExps :: DDefs0 -> Subst -> Gamma -> Gamma -> [TyVar]
       -> [(Bool, Exp0)] -> TcM (Subst, [Ty0], [Exp0])
tcExps :: DDefs0
-> Subst
-> Map Var TyScheme
-> Map Var TyScheme
-> [TyVar]
-> [(Bool, Exp0)]
-> TcM (Subst, [Ty0], [Exp0])
tcExps DDefs0
ddefs Subst
sbst Map Var TyScheme
venv Map Var TyScheme
fenv [TyVar]
bound_tyvars [(Bool, Exp0)]
ls = do
  ([Subst]
sbsts,[Ty0]
tys,[Exp0]
exps) <- [(Subst, Ty0, Exp0)] -> ([Subst], [Ty0], [Exp0])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 ([(Subst, Ty0, Exp0)] -> ([Subst], [Ty0], [Exp0]))
-> TcM [(Subst, Ty0, Exp0)] -> TcM ([Subst], [Ty0], [Exp0])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Bool, Exp0) -> TcM (Subst, Ty0, Exp0))
-> [(Bool, Exp0)] -> TcM [(Subst, Ty0, Exp0)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Bool, Exp0) -> TcM (Subst, Ty0, Exp0)
go [(Bool, Exp0)]
ls
  (Subst, [Ty0], [Exp0]) -> TcM (Subst, [Ty0], [Exp0])
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Subst -> Subst -> Subst) -> Subst -> [Subst] -> Subst
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
(<>) Subst
sbst [Subst]
sbsts, [Ty0]
tys, [Exp0]
exps)
  where
    go :: (Bool, Exp0) -> TcM (Subst, Ty0, Exp0)
go (Bool
is_main, Exp0
e) = DDefs0
-> Subst
-> Map Var TyScheme
-> Map Var TyScheme
-> [TyVar]
-> Bool
-> Exp0
-> TcM (Subst, Ty0, Exp0)
tcExp DDefs0
ddefs Subst
sbst Map Var TyScheme
venv Map Var TyScheme
fenv [TyVar]
bound_tyvars Bool
is_main Exp0
e

--
tcExp :: DDefs0 -> Subst -> Gamma -> Gamma -> [TyVar]
      -> Bool -> Exp0 -> TcM (Subst, Ty0, Exp0)
tcExp :: DDefs0
-> Subst
-> Map Var TyScheme
-> Map Var TyScheme
-> [TyVar]
-> Bool
-> Exp0
-> TcM (Subst, Ty0, Exp0)
tcExp DDefs0
ddefs Subst
sbst Map Var TyScheme
venv Map Var TyScheme
fenv [TyVar]
bound_tyvars Bool
is_main Exp0
ex = (\(Subst
a,Ty0
b,Exp0
c) -> (Subst
a,Ty0
b,Exp0
c)) ((Subst, Ty0, Exp0) -> (Subst, Ty0, Exp0))
-> TcM (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
  case Exp0
ex of
    VarE Var
x -> do
      ([Ty0]
metas, Ty0
ty) <-
        case (Var -> Map Var TyScheme -> Maybe TyScheme
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
x Map Var TyScheme
venv, Var -> Map Var TyScheme -> Maybe TyScheme
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
x Map Var TyScheme
fenv) of
          (Maybe TyScheme
Nothing, Maybe TyScheme
Nothing) -> Doc -> TcM ([Ty0], Ty0)
forall a. Doc -> TcM a
err (Doc -> TcM ([Ty0], Ty0)) -> Doc -> TcM ([Ty0], Ty0)
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Unbound variable " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Var -> Doc
forall a. Out a => a -> Doc
doc Var
x
          (Just TyScheme
t, Maybe TyScheme
_) -> TyScheme -> TcM ([Ty0], Ty0)
instantiate TyScheme
t
          (Maybe TyScheme
_, Just TyScheme
t) -> TyScheme -> TcM ([Ty0], Ty0)
instantiate TyScheme
t
      if Ty0 -> Bool
isFunTy Ty0
ty
      then (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
sbst, Ty0
ty, E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext (E0Ext Ty0 Ty0 -> Exp0) -> E0Ext Ty0 Ty0 -> Exp0
forall a b. (a -> b) -> a -> b
$ [Ty0] -> Var -> E0Ext Ty0 Ty0
forall loc dec. [loc] -> Var -> E0Ext loc dec
FunRefE [Ty0]
metas Var
x)
      else (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
sbst, Ty0
ty, Var -> Exp0
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
x)

    LitE{}    -> (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
sbst, Ty0
IntTy, Exp0
ex)
    CharE{}   -> (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
sbst, Ty0
CharTy, Exp0
ex)
    FloatE{}  -> (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
sbst, Ty0
FloatTy, Exp0
ex)
    LitSymE{} -> (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
sbst, Ty0
SymTy0, Exp0
ex)

    AppE Var
f [Ty0]
_tyapps [Exp0]
args -> do
      (TyScheme
sigma, ([Ty0]
metas, Ty0
fn_ty_inst)) <-
        case (Var -> Map Var TyScheme -> Maybe TyScheme
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
f Map Var TyScheme
venv, Var -> Map Var TyScheme -> Maybe TyScheme
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
f Map Var TyScheme
fenv) of
          (Just TyScheme
lam_ty, Maybe TyScheme
_) -> (TyScheme
lam_ty,) (([Ty0], Ty0) -> (TyScheme, ([Ty0], Ty0)))
-> TcM ([Ty0], Ty0) -> TcM (TyScheme, ([Ty0], Ty0))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyScheme -> TcM ([Ty0], Ty0)
instantiate TyScheme
lam_ty
          (Maybe TyScheme
_, Just TyScheme
fn_ty)  -> (TyScheme
fn_ty,) (([Ty0], Ty0) -> (TyScheme, ([Ty0], Ty0)))
-> TcM ([Ty0], Ty0) -> TcM (TyScheme, ([Ty0], Ty0))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyScheme -> TcM ([Ty0], Ty0)
instantiate TyScheme
fn_ty
          (Maybe TyScheme, Maybe TyScheme)
_ -> Doc -> TcM (TyScheme, ([Ty0], Ty0))
forall a. Doc -> TcM a
err (Doc -> TcM (TyScheme, ([Ty0], Ty0)))
-> Doc -> TcM (TyScheme, ([Ty0], Ty0))
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Unknown function:" Doc -> Doc -> Doc
<+> Var -> Doc
forall a. Out a => a -> Doc
doc Var
f

      if TyScheme -> [Exp0] -> Bool
isCallUnsaturated TyScheme
sigma [Exp0]
args
      then do
        Exp0
e' <- TyScheme -> Exp0 -> TcM Exp0
forall (m :: * -> *).
MonadState Int m =>
TyScheme -> Exp0 -> m Exp0
saturateCall TyScheme
sigma Exp0
ex
        (Subst
s1, Ty0
e_ty, Exp0
e'') <- DDefs0
-> Subst
-> Map Var TyScheme
-> Map Var TyScheme
-> [TyVar]
-> Bool
-> Exp0
-> TcM (Subst, Ty0, Exp0)
tcExp DDefs0
ddefs Subst
sbst Map Var TyScheme
venv Map Var TyScheme
fenv [TyVar]
bound_tyvars Bool
is_main Exp0
e'
        (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1, Ty0
e_ty, Exp0
e'')
      else do
        (Subst
s2, [Ty0]
arg_tys, [Exp0]
args_tc) <- DDefs0
-> Subst
-> Map Var TyScheme
-> Map Var TyScheme
-> [TyVar]
-> [(Bool, Exp0)]
-> TcM (Subst, [Ty0], [Exp0])
tcExps DDefs0
ddefs Subst
sbst Map Var TyScheme
venv Map Var TyScheme
fenv [TyVar]
bound_tyvars ([Bool] -> [Exp0] -> [(Bool, Exp0)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
is_main) [Exp0]
args)
        -- let fn_ty_inst' = zonkTy s2 fn_ty_inst
        let fn_ty_inst' :: Ty0
fn_ty_inst' = Ty0
fn_ty_inst
        Subst
s3 <- Exp0 -> [Ty0] -> [Ty0] -> TcM Subst
unifyl Exp0
ex (Ty0 -> [Ty0]
arrIns' Ty0
fn_ty_inst') [Ty0]
arg_tys
        Ty0
fresh <- TcM Ty0
forall (m :: * -> *). MonadState Int m => m Ty0
newMetaTy
        Subst
s4 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify Exp0
ex ([Ty0] -> Ty0 -> Ty0
ArrowTy [Ty0]
arg_tys Ty0
fresh) Ty0
fn_ty_inst'
        -- Fill in type applications for specialization...
        --     id 10 ===> id [Int] 10
        let tyapps :: [Ty0]
tyapps = (Ty0 -> Ty0) -> [Ty0] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Ty0 -> Ty0
zonkTy Subst
s3) [Ty0]
metas
            s5 :: Subst
s5 = Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s4
        (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s5, Subst -> Ty0 -> Ty0
zonkTy Subst
s5 Ty0
fresh, Var -> [Ty0] -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Var -> [loc] -> [PreExp ext loc dec] -> PreExp ext loc dec
AppE Var
f [Ty0]
tyapps ((Exp0 -> Exp0) -> [Exp0] -> [Exp0]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Exp0 -> Exp0
zonkExp Subst
s5) [Exp0]
args_tc))

    PrimAppE Prim Ty0
pr [Exp0]
args -> do
      (Subst
s1, [Ty0]
arg_tys, [Exp0]
args_tc) <- DDefs0
-> Subst
-> Map Var TyScheme
-> Map Var TyScheme
-> [TyVar]
-> [(Bool, Exp0)]
-> TcM (Subst, [Ty0], [Exp0])
tcExps DDefs0
ddefs Subst
sbst Map Var TyScheme
venv Map Var TyScheme
fenv [TyVar]
bound_tyvars ([Bool] -> [Exp0] -> [(Bool, Exp0)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
is_main) [Exp0]
args)
      let arg_tys' :: [Ty0]
arg_tys' = (Ty0 -> Ty0) -> [Ty0] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Ty0 -> Ty0
zonkTy Subst
s1) [Ty0]
arg_tys
          checkLen :: Int -> TcM ()
          checkLen :: Int -> TcM ()
checkLen Int
n =
            if [Exp0] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Exp0]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n
            then () -> TcM ()
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            else Doc -> TcM ()
forall a. Doc -> TcM a
err (Doc -> TcM ()) -> Doc -> TcM ()
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Wrong number of arguments to " Doc -> Doc -> Doc
<+> Prim Ty0 -> Doc
forall a. Out a => a -> Doc
doc Prim Ty0
pr Doc -> Doc -> Doc
<+> String -> Doc
text String
"."
                         Doc -> Doc -> Doc
$$ String -> Doc
text String
"Expected " Doc -> Doc -> Doc
<+> Int -> Doc
forall a. Out a => a -> Doc
doc Int
n
                         Doc -> Doc -> Doc
<+> String -> Doc
text String
", received " Doc -> Doc -> Doc
<+> Int -> Doc
forall a. Out a => a -> Doc
doc ([Exp0] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Exp0]
args)
                         Doc -> Doc -> Doc
$$ Doc
exp_doc
          len0 :: TcM ()
len0 = Int -> TcM ()
checkLen Int
0
          len1 :: TcM ()
len1 = Int -> TcM ()
checkLen Int
1
          len2 :: TcM ()
len2 = Int -> TcM ()
checkLen Int
2
          len3 :: TcM ()
len3 = Int -> TcM ()
checkLen Int
3
          len4 :: TcM ()
len4 = Int -> TcM ()
checkLen Int
4

          mk_bools :: TcM (Subst, Ty0, Exp0)
mk_bools = do
            TcM ()
len0
            (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1, Ty0
BoolTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

          bool_ops :: TcM (Subst, Ty0, Exp0)
bool_ops = do
            TcM ()
len2
            Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
BoolTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
            Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
BoolTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
            (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3, Ty0
BoolTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

          int_ops :: TcM (Subst, Ty0, Exp0)
int_ops = do
            TcM ()
len2
            Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
IntTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
            Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
IntTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
            (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3, Ty0
IntTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

          int_cmps :: TcM (Subst, Ty0, Exp0)
int_cmps = do
            TcM ()
len2
            Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
IntTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
            Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
IntTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
            (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3, Ty0
BoolTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

          float_ops :: TcM (Subst, Ty0, Exp0)
float_ops = do
            TcM ()
len2
            Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
FloatTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
            Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
FloatTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
            (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3, Ty0
FloatTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

          float_cmps :: TcM (Subst, Ty0, Exp0)
float_cmps = do
            TcM ()
len2
            Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
FloatTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
            Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
FloatTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
            (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3, Ty0
BoolTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)
          
          char_cmps :: TcM (Subst, Ty0, Exp0)
char_cmps = do
            TcM ()
len2
            Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
CharTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
            Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
CharTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
            (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3, Ty0
BoolTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

      case Prim Ty0
pr of
        Prim Ty0
MkTrue  -> TcM (Subst, Ty0, Exp0)
mk_bools
        Prim Ty0
MkFalse -> TcM (Subst, Ty0, Exp0)
mk_bools
        Prim Ty0
AddP    -> TcM (Subst, Ty0, Exp0)
int_ops
        Prim Ty0
SubP    -> TcM (Subst, Ty0, Exp0)
int_ops
        Prim Ty0
MulP    -> TcM (Subst, Ty0, Exp0)
int_ops
        Prim Ty0
DivP    -> TcM (Subst, Ty0, Exp0)
int_ops
        Prim Ty0
ModP    -> TcM (Subst, Ty0, Exp0)
int_ops
        Prim Ty0
ExpP    -> TcM (Subst, Ty0, Exp0)
int_ops
        Prim Ty0
FAddP   -> TcM (Subst, Ty0, Exp0)
float_ops
        Prim Ty0
FSubP   -> TcM (Subst, Ty0, Exp0)
float_ops
        Prim Ty0
FMulP   -> TcM (Subst, Ty0, Exp0)
float_ops
        Prim Ty0
FDivP   -> TcM (Subst, Ty0, Exp0)
float_ops
        Prim Ty0
FExpP   -> TcM (Subst, Ty0, Exp0)
float_ops
        Prim Ty0
EqIntP  -> TcM (Subst, Ty0, Exp0)
int_cmps
        Prim Ty0
LtP     -> TcM (Subst, Ty0, Exp0)
int_cmps
        Prim Ty0
GtP     -> TcM (Subst, Ty0, Exp0)
int_cmps
        Prim Ty0
LtEqP   -> TcM (Subst, Ty0, Exp0)
int_cmps
        Prim Ty0
GtEqP   -> TcM (Subst, Ty0, Exp0)
int_cmps
        Prim Ty0
EqFloatP -> TcM (Subst, Ty0, Exp0)
float_cmps
        Prim Ty0
EqCharP  -> TcM (Subst, Ty0, Exp0)
char_cmps
        Prim Ty0
FLtP     -> TcM (Subst, Ty0, Exp0)
float_cmps
        Prim Ty0
FGtP     -> TcM (Subst, Ty0, Exp0)
float_cmps
        Prim Ty0
FLtEqP   -> TcM (Subst, Ty0, Exp0)
float_cmps
        Prim Ty0
FGtEqP   -> TcM (Subst, Ty0, Exp0)
float_cmps
        Prim Ty0
OrP     -> TcM (Subst, Ty0, Exp0)
bool_ops
        Prim Ty0
AndP    -> TcM (Subst, Ty0, Exp0)
bool_ops

        Prim Ty0
Gensym -> TcM ()
len0 TcM () -> (() -> TcM (Subst, Ty0, Exp0)) -> TcM (Subst, Ty0, Exp0)
forall a b. TcM a -> (a -> TcM b) -> TcM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \()
_ -> (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
sbst, Ty0
SymTy0, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
EqSymP -> do
          TcM ()
len2
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
SymTy0 ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
          Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
SymTy0 ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3, Ty0
BoolTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        EqBenchProgP String
_ -> do
          TcM ()
len0
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1, Ty0
BoolTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
RandP -> (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1, Ty0
IntTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)
        Prim Ty0
FRandP-> (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1, Ty0
FloatTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)
        Prim Ty0
FSqrtP -> do
          TcM ()
len1
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
FloatTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, Ty0
FloatTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
FTanP -> do
          TcM ()
len1
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
FloatTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, Ty0
FloatTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
FloatToIntP -> do
          TcM ()
len1
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
FloatTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, Ty0
IntTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
IntToFloatP -> do
          TcM ()
len1
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
IntTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, Ty0
FloatTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
PrintInt -> do
          TcM ()
len1
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
IntTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, [Ty0] -> Ty0
ProdTy [], Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
PrintChar -> do
          TcM ()
len1
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
CharTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, [Ty0] -> Ty0
ProdTy [], Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
PrintFloat -> do
          TcM ()
len1
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
FloatTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, [Ty0] -> Ty0
ProdTy [], Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
PrintBool -> do
          TcM ()
len1
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
BoolTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, [Ty0] -> Ty0
ProdTy [], Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
PrintSym -> do
          TcM ()
len1
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
SymTy0 ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, [Ty0] -> Ty0
ProdTy [], Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
ReadInt -> do
          TcM ()
len0
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1, Ty0
IntTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
SymSetEmpty -> do
          TcM ()
len0
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1, Ty0
SymSetTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
SymSetInsert -> do
          TcM ()
len2
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
SymSetTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
          Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
SymTy0 ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3, Ty0
SymSetTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
SymSetContains -> do
          TcM ()
len2
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
SymSetTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
          Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
SymTy0 ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3, Ty0
BoolTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
SymHashEmpty -> do
          TcM ()
len0
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1, Ty0
SymHashTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
SymHashInsert -> do
          TcM ()
len3
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
SymHashTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
          Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
SymTy0 ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
          Subst
s4 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
2) Ty0
SymTy0 ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s4, Ty0
SymHashTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
SymHashLookup -> do
          TcM ()
len2
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
SymHashTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
          Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
SymTy0 ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3, Ty0
SymTy0, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
SymHashContains -> do
          TcM ()
len2
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
SymHashTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
          Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
SymTy0 ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3, Ty0
BoolTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        DictEmptyP Ty0
ty -> do
          TcM ()
len1
          let [Ty0
a] = [Ty0]
arg_tys'
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
ArenaTy Ty0
a
          case [Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0 of
            (VarE Var
var) ->
                (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, Maybe Var -> Ty0 -> Ty0
SymDictTy (Var -> Maybe Var
forall a. a -> Maybe a
Just Var
var) Ty0
ty,
                         Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)
            Ext (L Loc
_ (VarE Var
var)) ->
                (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, Maybe Var -> Ty0 -> Ty0
SymDictTy (Var -> Maybe Var
forall a. a -> Maybe a
Just Var
var) Ty0
ty,
                         Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)
            Exp0
_ -> Doc -> TcM (Subst, Ty0, Exp0)
forall a. Doc -> TcM a
err (Doc -> TcM (Subst, Ty0, Exp0)) -> Doc -> TcM (Subst, Ty0, Exp0)
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Expected arena variable argument in: " Doc -> Doc -> Doc
<+> Doc
exp_doc

        DictInsertP Ty0
ty -> do
          TcM ()
len4
          let [Ty0
a,Ty0
d,Ty0
k,Ty0
v] = [Ty0]
arg_tys'
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) (Maybe Var -> Ty0 -> Ty0
SymDictTy Maybe Var
forall a. Maybe a
Nothing Ty0
ty) Ty0
d
          Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
2) Ty0
SymTy0 Ty0
k
          Subst
s4 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
3) Ty0
ty Ty0
v
          Subst
s5 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
ArenaTy Ty0
a
          case [Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0 of
            (VarE Var
var) -> (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s4 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s5,
                                       Maybe Var -> Ty0 -> Ty0
SymDictTy (Var -> Maybe Var
forall a. a -> Maybe a
Just Var
var) Ty0
ty,
                                       Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)
            Ext (L Loc
_ (VarE Var
var)) -> (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s4 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s5,
                                       Maybe Var -> Ty0 -> Ty0
SymDictTy (Var -> Maybe Var
forall a. a -> Maybe a
Just Var
var) Ty0
ty,
                                       Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)
            Exp0
_ -> Doc -> TcM (Subst, Ty0, Exp0)
forall a. Doc -> TcM a
err (Doc -> TcM (Subst, Ty0, Exp0)) -> Doc -> TcM (Subst, Ty0, Exp0)
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Expected arena variable argument in: " Doc -> Doc -> Doc
<+> Doc
exp_doc

        DictLookupP Ty0
ty -> do
          TcM ()
len2
          let [Ty0
d,Ty0
k] = [Ty0]
arg_tys'
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Maybe Var -> Ty0 -> Ty0
SymDictTy Maybe Var
forall a. Maybe a
Nothing Ty0
ty) Ty0
d
          Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
SymTy0 Ty0
k
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3, Ty0
ty, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        DictHasKeyP Ty0
ty -> do
          TcM ()
len2
          let [Ty0
d,Ty0
k] = [Ty0]
arg_tys'
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Maybe Var -> Ty0 -> Ty0
SymDictTy Maybe Var
forall a. Maybe a
Nothing Ty0
ty) Ty0
d
          Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
SymTy0 Ty0
k
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3, Ty0
BoolTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
IntHashEmpty -> do
          TcM ()
len0
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1, Ty0
IntHashTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
IntHashInsert -> do
          TcM ()
len3
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
IntHashTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
          Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
SymTy0 ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
          Subst
s4 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
2) Ty0
IntTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s4, Ty0
IntHashTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
IntHashLookup -> do
          TcM ()
len2
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
IntHashTy ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
          Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
SymTy0 ([Ty0]
arg_tys' [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3, Ty0
IntTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        VAllocP Ty0
elty -> do
          TcM ()
len1
          let [Ty0
i] = [Ty0]
arg_tys'
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
IntTy Ty0
i
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, Ty0 -> Ty0
VectorTy Ty0
elty, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        VFreeP Ty0
elty -> do
          TcM ()
len1
          let [Ty0
i] = [Ty0]
arg_tys'
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Ty0 -> Ty0
VectorTy Ty0
elty) Ty0
i
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, [Ty0] -> Ty0
ProdTy [], Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        VFree2P Ty0
elty -> do
          TcM ()
len1
          let [Ty0
i] = [Ty0]
arg_tys'
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Ty0 -> Ty0
VectorTy Ty0
elty) Ty0
i
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, [Ty0] -> Ty0
ProdTy [], Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        VLengthP Ty0
elty -> do
          TcM ()
len1
          let [Ty0
ls] = [Ty0]
arg_tys'
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Ty0 -> Ty0
VectorTy Ty0
elty) Ty0
ls
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, Ty0
IntTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        VNthP Ty0
elty -> do
          TcM ()
len2
          let [Ty0
ls,Ty0
i] = [Ty0]
arg_tys'
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Ty0 -> Ty0
VectorTy Ty0
elty) Ty0
ls
          Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
IntTy Ty0
i
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3, Ty0
elty, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        VSliceP Ty0
elty -> do
          TcM ()
len3
          let [Ty0
from,Ty0
to,Ty0
ls] = [Ty0]
arg_tys'
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
IntTy Ty0
from
          Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
IntTy Ty0
to
          Subst
s4 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
2) (Ty0 -> Ty0
VectorTy Ty0
elty) Ty0
ls
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s4, Ty0 -> Ty0
VectorTy Ty0
elty, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        InplaceVUpdateP Ty0
elty -> do
          TcM ()
len3
          let [Ty0
ls,Ty0
i,Ty0
val] = [Ty0]
arg_tys'
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Ty0 -> Ty0
VectorTy Ty0
elty) Ty0
ls
          Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
IntTy Ty0
i
          Subst
s4 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
2) Ty0
elty Ty0
val
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s4, Ty0 -> Ty0
VectorTy Ty0
elty, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        VConcatP Ty0
elty -> do
          TcM ()
len1
          let [Ty0
ls] = [Ty0]
arg_tys'
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Ty0 -> Ty0
VectorTy (Ty0 -> Ty0
VectorTy Ty0
elty)) Ty0
ls
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, Ty0 -> Ty0
VectorTy Ty0
elty, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        -- Given that the first argument is a list of type (VectorTy t),
        -- ensure that the 2nd argument is function reference of type:
        -- ty -> ty -> IntTy
        --
        -- TODO: cannot unify if the 2nd argument is a lambda.
        VSortP Ty0
elty -> do
          TcM ()
len2
          let [Ty0
ls,Ty0
fp] = [Ty0]
arg_tys'
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Ty0 -> Ty0
VectorTy Ty0
elty) Ty0
ls
          Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) ([Ty0] -> Ty0 -> Ty0
ArrowTy [Ty0
elty, Ty0
elty] Ty0
IntTy) Ty0
fp
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3, Ty0 -> Ty0
VectorTy Ty0
elty, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        InplaceVSortP Ty0
elty -> do
          (Subst
s2, Ty0
t, Exp0
e) <- Exp0 -> TcM (Subst, Ty0, Exp0)
go (Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE (Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
VSortP Ty0
elty) [Exp0]
args)
          case Exp0
e of
            PrimAppE (VSortP Ty0
t2) [Exp0]
args2 ->
              (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, Ty0
t, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE (Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
InplaceVSortP Ty0
t2) [Exp0]
args2)
            Exp0
_ -> Doc -> TcM (Subst, Ty0, Exp0)
forall a. Doc -> TcM a
err (Doc -> TcM (Subst, Ty0, Exp0)) -> Doc -> TcM (Subst, Ty0, Exp0)
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"InPlaceVSortP"

        VMergeP Ty0
elty -> do
          TcM ()
len2
          let [Ty0
ls1,Ty0
ls2] = [Ty0]
arg_tys'
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Ty0 -> Ty0
VectorTy Ty0
elty) Ty0
ls1
          Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) (Ty0 -> Ty0
VectorTy Ty0
elty) Ty0
ls2
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3, Ty0 -> Ty0
VectorTy Ty0
elty, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        PDictInsertP Ty0
kty Ty0
vty -> do
          TcM ()
len3
          let [Ty0
key, Ty0
val, Ty0
dict] = [Ty0]
arg_tys'
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
key Ty0
kty
          Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
val Ty0
vty
          Subst
s4 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
2) Ty0
dict (Ty0 -> Ty0 -> Ty0
PDictTy Ty0
kty Ty0
vty)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s4, Ty0 -> Ty0 -> Ty0
PDictTy Ty0
kty Ty0
vty, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        PDictLookupP Ty0
kty Ty0
vty -> do
          TcM ()
len2
          let [Ty0
key, Ty0
dict] = [Ty0]
arg_tys'
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
key Ty0
kty
          Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
dict (Ty0 -> Ty0 -> Ty0
PDictTy Ty0
kty Ty0
vty)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3, Ty0
vty, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        PDictAllocP Ty0
kty Ty0
vty -> do
          TcM ()
len0
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1, Ty0 -> Ty0 -> Ty0
PDictTy Ty0
kty Ty0
vty, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        PDictHasKeyP Ty0
kty Ty0
vty -> do
          TcM ()
len2
          let [Ty0
key, Ty0
dict] = [Ty0]
arg_tys'
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
key Ty0
kty
          Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
dict (Ty0 -> Ty0 -> Ty0
PDictTy Ty0
kty Ty0
vty)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3, Ty0
BoolTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        PDictForkP Ty0
kty Ty0
vty -> do
          TcM ()
len1
          let [Ty0
dict] = [Ty0]
arg_tys'
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
dict (Ty0 -> Ty0 -> Ty0
PDictTy Ty0
kty Ty0
vty)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, [Ty0] -> Ty0
ProdTy [Ty0 -> Ty0 -> Ty0
PDictTy Ty0
kty Ty0
vty, Ty0 -> Ty0 -> Ty0
PDictTy Ty0
kty Ty0
vty], Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        PDictJoinP Ty0
kty Ty0
vty -> do
          TcM ()
len2
          let [Ty0
dict1, Ty0
dict2] = [Ty0]
arg_tys'
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
dict1 (Ty0 -> Ty0 -> Ty0
PDictTy Ty0
kty Ty0
vty)
          Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
dict2 (Ty0 -> Ty0 -> Ty0
PDictTy Ty0
kty Ty0
vty)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3, Ty0 -> Ty0 -> Ty0
PDictTy Ty0
kty Ty0
vty, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        LLAllocP Ty0
elty -> do
          TcM ()
len0
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1, Ty0 -> Ty0
ListTy Ty0
elty, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        LLIsEmptyP Ty0
elty -> do
          TcM ()
len1
          let [Ty0
ll] = [Ty0]
arg_tys
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
ll (Ty0 -> Ty0
ListTy Ty0
elty)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, Ty0
BoolTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        LLConsP Ty0
elty -> do
          TcM ()
len2
          let [Ty0
elt, Ty0
ll] = [Ty0]
arg_tys
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
elt Ty0
elty
          Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) Ty0
ll (Ty0 -> Ty0
ListTy Ty0
elty)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3, Ty0 -> Ty0
ListTy Ty0
elty, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        LLHeadP Ty0
elty -> do
          TcM ()
len1
          let [Ty0
ll] = [Ty0]
arg_tys
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
ll (Ty0 -> Ty0
ListTy Ty0
elty)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, Ty0
elty, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        LLTailP Ty0
elty -> do
          TcM ()
len1
          let [Ty0
ll] = [Ty0]
arg_tys
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
ll (Ty0 -> Ty0
ListTy Ty0
elty)
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, Ty0 -> Ty0
ListTy Ty0
elty, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        LLFreeP Ty0
elty -> do
          TcM ()
len1
          let [Ty0
i] = [Ty0]
arg_tys'
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Ty0 -> Ty0
ListTy Ty0
elty) Ty0
i
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, [Ty0] -> Ty0
ProdTy [], Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        LLFree2P Ty0
elty -> do
          TcM ()
len1
          let [Ty0
i] = [Ty0]
arg_tys'
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Ty0 -> Ty0
ListTy Ty0
elty) Ty0
i
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, [Ty0] -> Ty0
ProdTy [], Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        LLCopyP Ty0
elty -> do
          TcM ()
len1
          let [Ty0
i] = [Ty0]
arg_tys'
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) (Ty0 -> Ty0
ListTy Ty0
elty) Ty0
i
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, Ty0 -> Ty0
ListTy Ty0
elty, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
GetNumProcessors -> do
          TcM ()
len0
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1, Ty0
IntTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        ErrorP String
_str Ty0
ty -> do
          TcM ()
len0
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1, Ty0
ty, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
SizeParam -> do
          TcM ()
len0
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1, Ty0
IntTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        Prim Ty0
IsBig -> do
          TcM ()
len2
          let [Ty0
ity, Ty0
_ety] = [Ty0]
arg_tys'
          -- s1 <- unify (args !! 0) (PackedTy)
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
IntTy Ty0
ity
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, Ty0
BoolTy, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        ReadPackedFile Maybe String
_fp String
_tycon Maybe Var
_reg Ty0
ty -> do
          TcM ()
len0
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1, Ty0
ty, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        ReadArrayFile Maybe (String, Int)
_ Ty0
ty -> do
          TcM ()
len0
          (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1, Ty0 -> Ty0
VectorTy Ty0
ty, Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr [Exp0]
args_tc)

        WritePackedFile String
fp Ty0
ty -> do
             TcM ()
len1
             let [Ty0
packed_ty] = [Ty0]
arg_tys'
             Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify ([Exp0]
args [Exp0] -> Int -> Exp0
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) Ty0
ty Ty0
packed_ty
             (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, [Ty0] -> Ty0
ProdTy [], Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE (String -> Ty0 -> Prim Ty0
forall ty. String -> ty -> Prim ty
WritePackedFile String
fp (Subst -> Ty0 -> Ty0
zonkTy Subst
s2 Ty0
ty)) [Exp0]
args_tc)

        Write3dPpmFile{} -> Doc -> TcM (Subst, Ty0, Exp0)
forall a. Doc -> TcM a
err (Doc -> TcM (Subst, Ty0, Exp0)) -> Doc -> TcM (Subst, Ty0, Exp0)
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Write3dPpmFile"
        Prim Ty0
RequestSizeOf-> Doc -> TcM (Subst, Ty0, Exp0)
forall a. Doc -> TcM a
err (Doc -> TcM (Subst, Ty0, Exp0)) -> Doc -> TcM (Subst, Ty0, Exp0)
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Unexpected RequestSizeOf in L0: " Doc -> Doc -> Doc
<+> Doc
exp_doc
        Prim Ty0
RequestEndOf -> Doc -> TcM (Subst, Ty0, Exp0)
forall a. Doc -> TcM a
err (Doc -> TcM (Subst, Ty0, Exp0)) -> Doc -> TcM (Subst, Ty0, Exp0)
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Unexpected RequestEndOf in L0: " Doc -> Doc -> Doc
<+> Doc
exp_doc


    LetE (Var
v, [], Ty0
gvn_rhs_ty, Exp0
rhs) Exp0
bod -> do
      (Subst
s1, Ty0
drvd_rhs_ty, Exp0
rhs_tc) <- Exp0 -> TcM (Subst, Ty0, Exp0)
go Exp0
rhs
      Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify Exp0
rhs Ty0
gvn_rhs_ty Ty0
drvd_rhs_ty
      let s3 :: Subst
s3         = Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2
          venv' :: Map Var TyScheme
venv'      = Subst -> Map Var TyScheme -> Map Var TyScheme
zonkTyEnv Subst
s3 Map Var TyScheme
venv
          -- Added b/c Nothing :: Just Int
          drvd_rhs_ty' :: Ty0
drvd_rhs_ty' = Subst -> Ty0 -> Ty0
zonkTy Subst
s3 Ty0
drvd_rhs_ty
      (Subst
s4, TyScheme
rhs_ty_gen) <- Map Var TyScheme
-> Subst -> [TyVar] -> Ty0 -> TcM (Subst, TyScheme)
generalize Map Var TyScheme
venv' Subst
s3 [TyVar]
bound_tyvars Ty0
drvd_rhs_ty'
      let venv'' :: Map Var TyScheme
venv''     = Var -> TyScheme -> Map Var TyScheme -> Map Var TyScheme
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Var
v TyScheme
rhs_ty_gen Map Var TyScheme
venv'
      (Subst
s5, Ty0
bod_ty, Exp0
bod_tc) <- DDefs0
-> Subst
-> Map Var TyScheme
-> Map Var TyScheme
-> [TyVar]
-> Bool
-> Exp0
-> TcM (Subst, Ty0, Exp0)
tcExp DDefs0
ddefs Subst
s4 Map Var TyScheme
venv'' Map Var TyScheme
fenv [TyVar]
bound_tyvars Bool
is_main Exp0
bod
      (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s5, Ty0
bod_ty,
            (Var, [Ty0], Ty0, Exp0) -> Exp0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
(Var, [loc], dec, PreExp ext loc dec)
-> PreExp ext loc dec -> PreExp ext loc dec
LetE (Var
v, [], Subst -> Ty0 -> Ty0
zonkTy Subst
s4 Ty0
gvn_rhs_ty, Subst -> Exp0 -> Exp0
zonkExp Subst
s4 Exp0
rhs_tc) (Subst -> Exp0 -> Exp0
zonkExp Subst
s5 Exp0
bod_tc))

    LetE (Var
_, (Ty0
_:[Ty0]
_), Ty0
_, Exp0
_) Exp0
_ -> Doc -> TcM (Subst, Ty0, Exp0)
forall a. Doc -> TcM a
err (Doc -> TcM (Subst, Ty0, Exp0)) -> Doc -> TcM (Subst, Ty0, Exp0)
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Unexpected LetE: " Doc -> Doc -> Doc
<+> Doc
exp_doc

    IfE Exp0
a Exp0
b Exp0
c -> do
      (Subst
s1, Ty0
t1, Exp0
a_tc) <- Exp0 -> TcM (Subst, Ty0, Exp0)
go Exp0
a
      (Subst
s2, Ty0
t2, Exp0
b_tc) <- DDefs0
-> Subst
-> Map Var TyScheme
-> Map Var TyScheme
-> [TyVar]
-> Bool
-> Exp0
-> TcM (Subst, Ty0, Exp0)
tcExp DDefs0
ddefs Subst
s1 Map Var TyScheme
venv Map Var TyScheme
fenv [TyVar]
bound_tyvars Bool
is_main Exp0
b
      (Subst
s3, Ty0
t3, Exp0
c_tc) <- DDefs0
-> Subst
-> Map Var TyScheme
-> Map Var TyScheme
-> [TyVar]
-> Bool
-> Exp0
-> TcM (Subst, Ty0, Exp0)
tcExp DDefs0
ddefs Subst
s2 Map Var TyScheme
venv Map Var TyScheme
fenv [TyVar]
bound_tyvars Bool
is_main Exp0
c
      Subst
s4 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify Exp0
a Ty0
t1 Ty0
BoolTy
      Subst
s5 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify Exp0
ex Ty0
t2 Ty0
t3
      let s6 :: Subst
s6 = Subst
s3 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s4 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s5
      (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s6, Subst -> Ty0 -> Ty0
zonkTy Subst
s6 Ty0
t2,
            Exp0 -> Exp0 -> Exp0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
PreExp ext loc dec
-> PreExp ext loc dec -> PreExp ext loc dec -> PreExp ext loc dec
IfE (Subst -> Exp0 -> Exp0
zonkExp Subst
s6 Exp0
a_tc) (Subst -> Exp0 -> Exp0
zonkExp Subst
s6 Exp0
b_tc) (Subst -> Exp0 -> Exp0
zonkExp Subst
s6 Exp0
c_tc))

    MkProdE [Exp0]
es -> do
      (Subst
s1, [Ty0]
es_tys, [Exp0]
es_tc) <- DDefs0
-> Subst
-> Map Var TyScheme
-> Map Var TyScheme
-> [TyVar]
-> [(Bool, Exp0)]
-> TcM (Subst, [Ty0], [Exp0])
tcExps DDefs0
ddefs Subst
sbst Map Var TyScheme
venv Map Var TyScheme
fenv [TyVar]
bound_tyvars ([Bool] -> [Exp0] -> [(Bool, Exp0)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
is_main) [Exp0]
es)
      (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1, [Ty0] -> Ty0
ProdTy [Ty0]
es_tys, [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
[PreExp ext loc dec] -> PreExp ext loc dec
MkProdE [Exp0]
es_tc)

    ProjE Int
i Exp0
a -> do
     (Subst
s1, Ty0
a_ty, Exp0
a_tc) <- Exp0 -> TcM (Subst, Ty0, Exp0)
go Exp0
a
     case Subst -> Ty0 -> Ty0
zonkTy Subst
s1 Ty0
a_ty of
       ProdTy [Ty0]
tys -> (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1, [Ty0]
tys [Ty0] -> Int -> Ty0
forall a. HasCallStack => [a] -> Int -> a
!! Int
i, Int -> Exp0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
Int -> PreExp ext loc dec -> PreExp ext loc dec
ProjE Int
i Exp0
a_tc)
       Ty0
a_ty' -> Doc -> TcM (Subst, Ty0, Exp0)
forall a. Doc -> TcM a
err (Doc -> TcM (Subst, Ty0, Exp0)) -> Doc -> TcM (Subst, Ty0, Exp0)
forall a b. (a -> b) -> a -> b
$ Doc
"tcExp: Coulnd't match expected type: ProdTy [...]"
                      Doc -> Doc -> Doc
<+> Doc
"with actual type: " Doc -> Doc -> Doc
<+> Ty0 -> Doc
forall a. Out a => a -> Doc
doc Ty0
a_ty'
                      Doc -> Doc -> Doc
$$ Doc
exp_doc

    CaseE Exp0
scrt [(String, [(Var, Ty0)], Exp0)]
brs -> do
      (Subst
s1, Ty0
scrt_ty, Exp0
scrt_tc) <- Exp0 -> TcM (Subst, Ty0, Exp0)
go Exp0
scrt
      let scrt_ty' :: Ty0
scrt_ty' = Subst -> Ty0 -> Ty0
zonkTy Subst
s1 Ty0
scrt_ty
      case Ty0
scrt_ty' of
        (PackedTy String
tycon [Ty0]
drvd_tyargs) -> do
          let ddf :: DDef Ty0
ddf = DDefs0 -> String -> DDef Ty0
forall a. Out a => DDefs a -> String -> DDef a
lookupDDef DDefs0
ddefs String
tycon
          DDef Ty0
ddf' <- DDef Ty0 -> [Ty0] -> TcM (DDef Ty0)
substTyVarDDef DDef Ty0
ddf [Ty0]
drvd_tyargs
          [(String, [(Var, Ty0)], Exp0)]
brs' <- ((String, [(Var, Ty0)], Exp0)
 -> (String, [(Var, Ty0)], Exp0) -> Bool)
-> [(String, [(Var, Ty0)], Exp0)] -> [(String, [(Var, Ty0)], Exp0)]
forall a. (a -> a -> Bool) -> [a] -> [a]
L.nubBy (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
(==) (String -> String -> Bool)
-> ((String, [(Var, Ty0)], Exp0) -> String)
-> (String, [(Var, Ty0)], Exp0)
-> (String, [(Var, Ty0)], Exp0)
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (String, [(Var, Ty0)], Exp0) -> String
forall a b c. (a, b, c) -> a
fst3) ([(String, [(Var, Ty0)], Exp0)] -> [(String, [(Var, Ty0)], Exp0)])
-> ([[(String, [(Var, Ty0)], Exp0)]]
    -> [(String, [(Var, Ty0)], Exp0)])
-> [[(String, [(Var, Ty0)], Exp0)]]
-> [(String, [(Var, Ty0)], Exp0)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[(String, [(Var, Ty0)], Exp0)]] -> [(String, [(Var, Ty0)], Exp0)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(String, [(Var, Ty0)], Exp0)]]
 -> [(String, [(Var, Ty0)], Exp0)])
-> TcM [[(String, [(Var, Ty0)], Exp0)]]
-> TcM [(String, [(Var, Ty0)], Exp0)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((String, [(Var, Ty0)], Exp0)
 -> TcM [(String, [(Var, Ty0)], Exp0)])
-> [(String, [(Var, Ty0)], Exp0)]
-> TcM [[(String, [(Var, Ty0)], Exp0)]]
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 (\x :: (String, [(Var, Ty0)], Exp0)
x@(String
a,[(Var, Ty0)]
_,Exp0
c) -> 
              if String
a String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"_default" 
                then ((String, [(Bool, Ty0)]) -> TcM (String, [(Var, Ty0)], Exp0))
-> [(String, [(Bool, Ty0)])] -> TcM [(String, [(Var, Ty0)], Exp0)]
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 (\(String
a', [(Bool, Ty0)]
args) -> do
                        [(Var, Ty0)]
args' <- ((Bool, Ty0) -> TcM (Var, Ty0))
-> [(Bool, Ty0)] -> TcM [(Var, Ty0)]
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 ((Bool -> TcM Var)
-> (Ty0 -> TcM Ty0) -> (Bool, Ty0) -> TcM (Var, Ty0)
forall (f :: * -> *) a c b d.
Applicative f =>
(a -> f c) -> (b -> f d) -> (a, b) -> f (c, d)
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse (\Bool
_ -> Var -> TcM Var
forall (m :: * -> *). MonadState Int m => Var -> m Var
gensym Var
"wildcard") Ty0 -> TcM Ty0
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure) [(Bool, Ty0)]
args
                        (String, [(Var, Ty0)], Exp0) -> TcM (String, [(Var, Ty0)], Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
a', [(Var, Ty0)]
args', Exp0
c) 
                      ) (DDef Ty0 -> [(String, [(Bool, Ty0)])]
forall a. DDef a -> [(String, [(Bool, a)])]
dataCons DDef Ty0
ddf)
                else [(String, [(Var, Ty0)], Exp0)]
-> TcM [(String, [(Var, Ty0)], Exp0)]
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(String, [(Var, Ty0)], Exp0)
x]
            ) [(String, [(Var, Ty0)], Exp0)]
brs :: TcM [(DataCon, [(Var, Ty0)], Exp0)]
          let tycons_brs :: [String]
tycons_brs = ((String, [(Var, Ty0)], Exp0) -> String)
-> [(String, [(Var, Ty0)], Exp0)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (DDefs0 -> String -> String
forall a. Out a => DDefs a -> String -> String
getTyOfDataCon DDefs0
ddefs (String -> String)
-> ((String, [(Var, Ty0)], Exp0) -> String)
-> (String, [(Var, Ty0)], Exp0)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, [(Var, Ty0)], Exp0) -> String
forall a b c. (a, b, c) -> a
fst3) [(String, [(Var, Ty0)], Exp0)]
brs'
          case [String] -> [String]
forall a. Eq a => [a] -> [a]
L.nub [String]
tycons_brs of
            [String
one] -> if String
one String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
tycon
                     then do
                       (Subst
s2,Ty0
t2,[(String, [(Var, Ty0)], Exp0)]
brs_tc) <- DDefs0
-> Subst
-> Map Var TyScheme
-> Map Var TyScheme
-> [TyVar]
-> DDef Ty0
-> [(String, [(Var, Ty0)], Exp0)]
-> Bool
-> Exp0
-> TcM (Subst, Ty0, [(String, [(Var, Ty0)], Exp0)])
tcCases DDefs0
ddefs Subst
s1 Map Var TyScheme
venv Map Var TyScheme
fenv [TyVar]
bound_tyvars DDef Ty0
ddf' [(String, [(Var, Ty0)], Exp0)]
brs' Bool
is_main Exp0
ex
                       (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s2, Ty0
t2, Exp0 -> [(String, [(Var, Ty0)], Exp0)] -> Exp0
forall (ext :: * -> * -> *) loc dec.
PreExp ext loc dec
-> [(String, [(Var, loc)], PreExp ext loc dec)]
-> PreExp ext loc dec
CaseE Exp0
scrt_tc [(String, [(Var, Ty0)], Exp0)]
brs_tc)
                     else Doc -> TcM (Subst, Ty0, Exp0)
forall a. Doc -> TcM a
err (Doc -> TcM (Subst, Ty0, Exp0)) -> Doc -> TcM (Subst, Ty0, Exp0)
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Couldn't match" Doc -> Doc -> Doc
<+> String -> Doc
forall a. Out a => a -> Doc
doc String
one
                                Doc -> Doc -> Doc
<+> Doc
"with:" Doc -> Doc -> Doc
<+> Ty0 -> Doc
forall a. Out a => a -> Doc
doc Ty0
scrt_ty'
                                Doc -> Doc -> Doc
$$ Doc
exp_doc
            [String]
oth -> Doc -> TcM (Subst, Ty0, Exp0)
forall a. Doc -> TcM a
err (Doc -> TcM (Subst, Ty0, Exp0)) -> Doc -> TcM (Subst, Ty0, Exp0)
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Case clause constructors have mismatched types:"
                          Doc -> Doc -> Doc
<+> [String] -> Doc
forall a. Out a => a -> Doc
doc [String]
oth
                          Doc -> Doc -> Doc
$$ Doc
exp_doc
        Ty0
_ -> Doc -> TcM (Subst, Ty0, Exp0)
forall a. Doc -> TcM a
err (Doc -> TcM (Subst, Ty0, Exp0)) -> Doc -> TcM (Subst, Ty0, Exp0)
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Couldn't match" Doc -> Doc -> Doc
<+> Ty0 -> Doc
forall a. Out a => a -> Doc
doc Ty0
scrt_ty'
                     Doc -> Doc -> Doc
<+> Doc
"with a Packed type."
                     Doc -> Doc -> Doc
$$ Doc
exp_doc

    DataConE Ty0
_tyapps String
dcon [Exp0]
args -> do
      ([Ty0]
metas, [Ty0]
arg_tys_inst, Ty0
ret_ty_inst) <- DDefs0 -> String -> TcM ([Ty0], [Ty0], Ty0)
instDataConTy DDefs0
ddefs String
dcon
      (Subst
s1, [Ty0]
arg_tys, [Exp0]
args_tc) <- DDefs0
-> Subst
-> Map Var TyScheme
-> Map Var TyScheme
-> [TyVar]
-> [(Bool, Exp0)]
-> TcM (Subst, [Ty0], [Exp0])
tcExps DDefs0
ddefs Subst
sbst Map Var TyScheme
venv Map Var TyScheme
fenv [TyVar]
bound_tyvars ([Bool] -> [Exp0] -> [(Bool, Exp0)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
is_main) [Exp0]
args)
      Subst
s2 <- Exp0 -> [Ty0] -> [Ty0] -> TcM Subst
unifyl Exp0
ex [Ty0]
arg_tys_inst [Ty0]
arg_tys
      let s3 :: Subst
s3 = Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2
          tyapps :: Ty0
tyapps = [Ty0] -> Ty0
ProdTy ((Ty0 -> Ty0) -> [Ty0] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Ty0 -> Ty0
zonkTy Subst
s3) [Ty0]
metas)
      (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s3, Subst -> Ty0 -> Ty0
zonkTy Subst
s3 Ty0
ret_ty_inst,
            Ty0 -> String -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
loc -> String -> [PreExp ext loc dec] -> PreExp ext loc dec
DataConE Ty0
tyapps String
dcon ((Exp0 -> Exp0) -> [Exp0] -> [Exp0]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Exp0 -> Exp0
zonkExp Subst
s3) [Exp0]
args_tc))

    Ext (LambdaE [(Var, Ty0)]
args Exp0
bod) -> do
      ([Ty0]
freshs, Map Var TyScheme
venv', Subst
s3) <- (([Ty0], Map Var TyScheme, Subst)
 -> (Var, Ty0) -> TcM ([Ty0], Map Var TyScheme, Subst))
-> ([Ty0], Map Var TyScheme, Subst)
-> [(Var, Ty0)]
-> TcM ([Ty0], Map Var TyScheme, Subst)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM
                               (\([Ty0]
fs,Map Var TyScheme
env,Subst
s) (Var
v,Ty0
ty) -> do
                                 Ty0
fresh <- TcM Ty0
forall (m :: * -> *). MonadState Int m => m Ty0
newMetaTy
                                 let env' :: Map Var TyScheme
env' = Var -> TyScheme -> Map Var TyScheme -> Map Var TyScheme
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Var
v ([TyVar] -> Ty0 -> TyScheme
ForAll [] Ty0
fresh) Map Var TyScheme
env
                                 Subst
s1 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify (Var -> Exp0
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
v) Ty0
ty Ty0
fresh
                                 ([Ty0], Map Var TyScheme, Subst)
-> TcM ([Ty0], Map Var TyScheme, Subst)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Ty0]
fs [Ty0] -> [Ty0] -> [Ty0]
forall a. [a] -> [a] -> [a]
++ [Ty0
fresh], Map Var TyScheme
env', Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s))
                               ([],Map Var TyScheme
venv, Subst
sbst)
                               [(Var, Ty0)]
args
      (Subst
s4, Ty0
bod_ty, Exp0
bod_tc) <- DDefs0
-> Subst
-> Map Var TyScheme
-> Map Var TyScheme
-> [TyVar]
-> Bool
-> Exp0
-> TcM (Subst, Ty0, Exp0)
tcExp DDefs0
ddefs Subst
s3 Map Var TyScheme
venv' Map Var TyScheme
fenv [TyVar]
bound_tyvars Bool
is_main Exp0
bod
      (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
s4, Subst -> Ty0 -> Ty0
zonkTy Subst
s4 ([Ty0] -> Ty0 -> Ty0
ArrowTy [Ty0]
freshs Ty0
bod_ty),
              E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext ([(Var, Ty0)] -> Exp0 -> E0Ext Ty0 Ty0
forall loc dec.
[(Var, dec)] -> PreExp E0Ext loc dec -> E0Ext loc dec
LambdaE (((Var, Ty0) -> (Var, Ty0)) -> [(Var, Ty0)] -> [(Var, Ty0)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Var
v,Ty0
ty) -> (Var
v, Subst -> Ty0 -> Ty0
zonkTy Subst
s4 Ty0
ty)) [(Var, Ty0)]
args) (Subst -> Exp0 -> Exp0
zonkExp Subst
s4 Exp0
bod_tc)))

    Ext (PolyAppE Exp0
op Exp0
arg) -> do
      (Subst
s1, Ty0
t1, Exp0
op_tc) <- Exp0 -> TcM (Subst, Ty0, Exp0)
go Exp0
op
      (Subst
s2, Ty0
t2, Exp0
arg_tc) <- DDefs0
-> Subst
-> Map Var TyScheme
-> Map Var TyScheme
-> [TyVar]
-> Bool
-> Exp0
-> TcM (Subst, Ty0, Exp0)
tcExp DDefs0
ddefs Subst
s1 Map Var TyScheme
venv Map Var TyScheme
fenv [TyVar]
bound_tyvars Bool
is_main Exp0
arg
      Ty0
fresh_out <- TcM Ty0
forall (m :: * -> *). MonadState Int m => m Ty0
newMetaTy
      let fresh_arrow :: Ty0
fresh_arrow = [Ty0] -> Ty0 -> Ty0
ArrowTy [Ty0
t2] Ty0
fresh_out
      Subst
s3 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify Exp0
op Ty0
t1 Ty0
fresh_arrow
      let s4 :: Subst
s4 = Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s3
      (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s4, Subst -> Ty0 -> Ty0
zonkTy Subst
s4 Ty0
fresh_out, 
        E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext (Exp0 -> Exp0 -> E0Ext Ty0 Ty0
forall loc dec.
PreExp E0Ext loc dec -> PreExp E0Ext loc dec -> E0Ext loc dec
PolyAppE (Subst -> Exp0 -> Exp0
zonkExp Subst
s4 Exp0
op_tc) (Subst -> Exp0 -> Exp0
zonkExp Subst
s4 Exp0
arg_tc)))

    Ext (FunRefE [Ty0]
tyapps Var
f) -> do
      ([Ty0]
_metas, Ty0
ty) <-
        case (Var -> Map Var TyScheme -> Maybe TyScheme
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
f Map Var TyScheme
venv, Var -> Map Var TyScheme -> Maybe TyScheme
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
f Map Var TyScheme
fenv) of
          (Maybe TyScheme
Nothing, Maybe TyScheme
Nothing) -> Doc -> TcM ([Ty0], Ty0)
forall a. Doc -> TcM a
err (Doc -> TcM ([Ty0], Ty0)) -> Doc -> TcM ([Ty0], Ty0)
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Unbound function " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Var -> Doc
forall a. Out a => a -> Doc
doc Var
f
          (Just TyScheme
t, Maybe TyScheme
_) -> TyScheme -> TcM ([Ty0], Ty0)
instantiate TyScheme
t
          (Maybe TyScheme
_, Just TyScheme
t) -> TyScheme -> TcM ([Ty0], Ty0)
instantiate TyScheme
t
      (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
sbst, Ty0
ty, E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext (E0Ext Ty0 Ty0 -> Exp0) -> E0Ext Ty0 Ty0 -> Exp0
forall a b. (a -> b) -> a -> b
$ [Ty0] -> Var -> E0Ext Ty0 Ty0
forall loc dec. [loc] -> Var -> E0Ext loc dec
FunRefE [Ty0]
tyapps Var
f)

    Ext (BenchE Var
fn [Ty0]
tyapps [Exp0]
args Bool
b) ->
      if Bool
is_main
      then do
        (Subst
s1, Ty0
ty, Exp0
e') <- Exp0 -> TcM (Subst, Ty0, Exp0)
go (Var -> [Ty0] -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Var -> [loc] -> [PreExp ext loc dec] -> PreExp ext loc dec
AppE Var
fn [Ty0]
tyapps [Exp0]
args)
        case Exp0
e' of
          AppE Var
fn' [Ty0]
tyapps' [Exp0]
args' ->
            (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1, Subst -> Ty0 -> Ty0
zonkTy Subst
s1 Ty0
ty, E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext (Var -> [Ty0] -> [Exp0] -> Bool -> E0Ext Ty0 Ty0
forall loc dec.
Var -> [loc] -> [PreExp E0Ext loc dec] -> Bool -> E0Ext loc dec
BenchE Var
fn' [Ty0]
tyapps' [Exp0]
args' Bool
b))
          Exp0
_ -> Doc -> TcM (Subst, Ty0, Exp0)
forall a. Doc -> TcM a
err (Doc -> TcM (Subst, Ty0, Exp0)) -> Doc -> TcM (Subst, Ty0, Exp0)
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"BenchE"
      else Doc -> TcM (Subst, Ty0, Exp0)
forall a. Doc -> TcM a
err (Doc -> TcM (Subst, Ty0, Exp0)) -> Doc -> TcM (Subst, Ty0, Exp0)
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"'bench' can only be used as a tail of the main expression." Doc -> Doc -> Doc
<+> Doc
exp_doc

    Ext (ParE0 [Exp0]
es)  -> do
      (Subst
s1, [Ty0]
es_tys, [Exp0]
es_tc) <- DDefs0
-> Subst
-> Map Var TyScheme
-> Map Var TyScheme
-> [TyVar]
-> [(Bool, Exp0)]
-> TcM (Subst, [Ty0], [Exp0])
tcExps DDefs0
ddefs Subst
sbst Map Var TyScheme
venv Map Var TyScheme
fenv [TyVar]
bound_tyvars ([Bool] -> [Exp0] -> [(Bool, Exp0)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
is_main) [Exp0]
es)
      (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1, [Ty0] -> Ty0
ProdTy [Ty0]
es_tys, E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext (E0Ext Ty0 Ty0 -> Exp0) -> E0Ext Ty0 Ty0 -> Exp0
forall a b. (a -> b) -> a -> b
$ [Exp0] -> E0Ext Ty0 Ty0
forall loc dec. [PreExp E0Ext loc dec] -> E0Ext loc dec
ParE0 [Exp0]
es_tc)

    Ext (PrintPacked Ty0
ty Exp0
arg) -> do
            (Subst
s1, Ty0
ty', Exp0
arg') <- Exp0 -> TcM (Subst, Ty0, Exp0)
go Exp0
arg
            Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify Exp0
arg Ty0
ty Ty0
ty'
            (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, [Ty0] -> Ty0
ProdTy [], E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext (Ty0 -> Exp0 -> E0Ext Ty0 Ty0
forall loc dec. dec -> PreExp E0Ext loc dec -> E0Ext loc dec
PrintPacked Ty0
ty Exp0
arg'))

    Ext (CopyPacked Ty0
ty Exp0
arg) -> do
            (Subst
s1, Ty0
ty', Exp0
arg') <- Exp0 -> TcM (Subst, Ty0, Exp0)
go Exp0
arg
            Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify Exp0
arg Ty0
ty Ty0
ty'
            (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, Ty0
ty', E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext (Ty0 -> Exp0 -> E0Ext Ty0 Ty0
forall loc dec. dec -> PreExp E0Ext loc dec -> E0Ext loc dec
CopyPacked Ty0
ty Exp0
arg'))

    Ext (TravPacked Ty0
ty Exp0
arg) -> do
            (Subst
s1, Ty0
ty', Exp0
arg') <- Exp0 -> TcM (Subst, Ty0, Exp0)
go Exp0
arg
            Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify Exp0
arg Ty0
ty Ty0
ty'
            (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, [Ty0] -> Ty0
ProdTy [], E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext (Ty0 -> Exp0 -> E0Ext Ty0 Ty0
forall loc dec. dec -> PreExp E0Ext loc dec -> E0Ext loc dec
TravPacked Ty0
ty Exp0
arg'))

    Ext (L Loc
_ Exp0
e) -> Exp0 -> TcM (Subst, Ty0, Exp0)
go Exp0
e

    Ext (LinearExt{}) -> Doc -> TcM (Subst, Ty0, Exp0)
forall a. Doc -> TcM a
err (Doc -> TcM (Subst, Ty0, Exp0)) -> Doc -> TcM (Subst, Ty0, Exp0)
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"a linear types extension wasn't desugared: " Doc -> Doc -> Doc
<+> Doc
exp_doc

    TimeIt Exp0
a Ty0
ty Bool
b -> do
      (Subst
s1, Ty0
ty', Exp0
a') <- Exp0 -> TcM (Subst, Ty0, Exp0)
go Exp0
a
      Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify Exp0
ex Ty0
ty Ty0
ty'
      let s3 :: Subst
s3 = Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2
      (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s3, Subst -> Ty0 -> Ty0
zonkTy Subst
s3 Ty0
ty', Exp0 -> Ty0 -> Bool -> Exp0
forall (ext :: * -> * -> *) loc dec.
PreExp ext loc dec -> dec -> Bool -> PreExp ext loc dec
TimeIt (Subst -> Exp0 -> Exp0
zonkExp Subst
s3 Exp0
a') (Subst -> Ty0 -> Ty0
zonkTy Subst
s3 Ty0
ty') Bool
b)

    WithArenaE Var
v Exp0
e1 -> do
      let venv' :: Map Var TyScheme
venv' = Var -> TyScheme -> Map Var TyScheme -> Map Var TyScheme
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Var
v ([TyVar] -> Ty0 -> TyScheme
ForAll [] Ty0
ArenaTy) Map Var TyScheme
venv
      (Subst
s1, Ty0
ty', Exp0
e1') <- DDefs0
-> Subst
-> Map Var TyScheme
-> Map Var TyScheme
-> [TyVar]
-> Bool
-> Exp0
-> TcM (Subst, Ty0, Exp0)
tcExp DDefs0
ddefs Subst
sbst Map Var TyScheme
venv' Map Var TyScheme
fenv [TyVar]
bound_tyvars Bool
is_main Exp0
e1
      (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1, Ty0
ty', Var -> Exp0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
Var -> PreExp ext loc dec -> PreExp ext loc dec
WithArenaE Var
v Exp0
e1')

    SpawnE Var
fn [Ty0]
tyapps [Exp0]
args -> do
      (Subst
s1, Ty0
ty, Exp0
e') <- DDefs0
-> Subst
-> Map Var TyScheme
-> Map Var TyScheme
-> [TyVar]
-> Bool
-> Exp0
-> TcM (Subst, Ty0, Exp0)
tcExp DDefs0
ddefs Subst
sbst Map Var TyScheme
venv Map Var TyScheme
fenv [TyVar]
bound_tyvars Bool
is_main (Var -> [Ty0] -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Var -> [loc] -> [PreExp ext loc dec] -> PreExp ext loc dec
AppE Var
fn [Ty0]
tyapps [Exp0]
args)
      case Exp0
e' of
        AppE Var
fn' [Ty0]
tyapps' [Exp0]
args' -> (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1, Ty0
ty, Var -> [Ty0] -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Var -> [loc] -> [PreExp ext loc dec] -> PreExp ext loc dec
SpawnE Var
fn' [Ty0]
tyapps' [Exp0]
args')
        Exp0
_ -> Doc -> TcM (Subst, Ty0, Exp0)
forall a. Doc -> TcM a
err (Doc -> TcM (Subst, Ty0, Exp0)) -> Doc -> TcM (Subst, Ty0, Exp0)
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"SpawnE: not a saturated function"

    Exp0
SyncE   -> (Subst, Ty0, Exp0) -> TcM (Subst, Ty0, Exp0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
sbst, [Ty0] -> Ty0
ProdTy [], Exp0
forall (ext :: * -> * -> *) loc dec. PreExp ext loc dec
SyncE)

    MapE{}  -> Doc -> TcM (Subst, Ty0, Exp0)
forall a. Doc -> TcM a
err (Doc -> TcM (Subst, Ty0, Exp0)) -> Doc -> TcM (Subst, Ty0, Exp0)
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"TODO" Doc -> Doc -> Doc
<+> Doc
exp_doc
    FoldE{} -> Doc -> TcM (Subst, Ty0, Exp0)
forall a. Doc -> TcM a
err (Doc -> TcM (Subst, Ty0, Exp0)) -> Doc -> TcM (Subst, Ty0, Exp0)
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"TODO" Doc -> Doc -> Doc
<+> Doc
exp_doc
  where
    go :: Exp0 -> TcM (Subst, Ty0, Exp0)
go = DDefs0
-> Subst
-> Map Var TyScheme
-> Map Var TyScheme
-> [TyVar]
-> Bool
-> Exp0
-> TcM (Subst, Ty0, Exp0)
tcExp DDefs0
ddefs Subst
sbst Map Var TyScheme
venv Map Var TyScheme
fenv [TyVar]
bound_tyvars Bool
is_main
    exp_doc :: Doc
exp_doc = Doc
"In the expression: " Doc -> Doc -> Doc
<+> Exp0 -> Doc
forall a. Out a => a -> Doc
doc Exp0
ex


tcCases :: DDefs0 -> Subst -> Gamma -> Gamma -> [TyVar]
        -> DDef0 -> [(DataCon, [(Var, Ty0)], Exp0)] -> Bool -> Exp0
        -> TcM (Subst, Ty0, [(DataCon, [(Var, Ty0)], Exp0)])
tcCases :: DDefs0
-> Subst
-> Map Var TyScheme
-> Map Var TyScheme
-> [TyVar]
-> DDef Ty0
-> [(String, [(Var, Ty0)], Exp0)]
-> Bool
-> Exp0
-> TcM (Subst, Ty0, [(String, [(Var, Ty0)], Exp0)])
tcCases DDefs0
ddefs Subst
sbst Map Var TyScheme
venv Map Var TyScheme
fenv [TyVar]
bound_tyvars DDef Ty0
ddf [(String, [(Var, Ty0)], Exp0)]
brs Bool
is_main Exp0
ex = do
  (Subst
s1,[Ty0]
tys,[(String, [(Var, Ty0)], Exp0)]
exps) <-
    ((Subst, [Ty0], [(String, [(Var, Ty0)], Exp0)])
 -> (String, [(Var, Ty0)], Exp0)
 -> TcM (Subst, [Ty0], [(String, [(Var, Ty0)], Exp0)]))
-> (Subst, [Ty0], [(String, [(Var, Ty0)], Exp0)])
-> [(String, [(Var, Ty0)], Exp0)]
-> TcM (Subst, [Ty0], [(String, [(Var, Ty0)], Exp0)])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM
      (\(Subst
s,[Ty0]
acc,[(String, [(Var, Ty0)], Exp0)]
ex_acc) (String
con,[(Var, Ty0)]
vtys,Exp0
rhs) -> do
        let vars :: [Var]
vars = ((Var, Ty0) -> Var) -> [(Var, Ty0)] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map (Var, Ty0) -> Var
forall a b. (a, b) -> a
fst [(Var, Ty0)]
vtys
            tys :: [Ty0]
tys  = DDef Ty0 -> String -> [Ty0]
forall a. Out a => DDef a -> String -> [a]
lookupDataCon' DDef Ty0
ddf String
con
            tys_gen :: [TyScheme]
tys_gen = (Ty0 -> TyScheme) -> [Ty0] -> [TyScheme]
forall a b. (a -> b) -> [a] -> [b]
map ([TyVar] -> Ty0 -> TyScheme
ForAll (DDef Ty0 -> [TyVar]
forall a. DDef a -> [TyVar]
tyArgs DDef Ty0
ddf [TyVar] -> [TyVar] -> [TyVar]
forall a. Eq a => [a] -> [a] -> [a]
L.\\ [TyVar]
bound_tyvars)) [Ty0]
tys
            venv' :: Map Var TyScheme
venv' = Map Var TyScheme
venv Map Var TyScheme -> Map Var TyScheme -> Map Var TyScheme
forall a. Semigroup a => a -> a -> a
<> ([(Var, TyScheme)] -> Map Var TyScheme
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Var, TyScheme)] -> Map Var TyScheme)
-> [(Var, TyScheme)] -> Map Var TyScheme
forall a b. (a -> b) -> a -> b
$ [Var] -> [TyScheme] -> [(Var, TyScheme)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
vars [TyScheme]
tys_gen)
            vtys' :: [(Var, Ty0)]
vtys' = [Var] -> [Ty0] -> [(Var, Ty0)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
vars [Ty0]
tys
        (Subst
s', Ty0
rhs_ty, Exp0
rhs_tc) <- DDefs0
-> Subst
-> Map Var TyScheme
-> Map Var TyScheme
-> [TyVar]
-> Bool
-> Exp0
-> TcM (Subst, Ty0, Exp0)
tcExp DDefs0
ddefs Subst
s Map Var TyScheme
venv' Map Var TyScheme
fenv [TyVar]
bound_tyvars Bool
is_main Exp0
rhs
        let rhs_ty' :: Ty0
rhs_ty' = Subst -> Ty0 -> Ty0
zonkTy Subst
s' Ty0
rhs_ty
            rhs_tc' :: Exp0
rhs_tc' = Subst -> Exp0 -> Exp0
zonkExp Subst
s' Exp0
rhs_tc
        (Subst, [Ty0], [(String, [(Var, Ty0)], Exp0)])
-> TcM (Subst, [Ty0], [(String, [(Var, Ty0)], Exp0)])
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s', [Ty0]
acc [Ty0] -> [Ty0] -> [Ty0]
forall a. [a] -> [a] -> [a]
++ [Ty0
rhs_ty'], [(String, [(Var, Ty0)], Exp0)]
ex_acc [(String, [(Var, Ty0)], Exp0)]
-> [(String, [(Var, Ty0)], Exp0)] -> [(String, [(Var, Ty0)], Exp0)]
forall a. [a] -> [a] -> [a]
++ [(String
con,[(Var, Ty0)]
vtys',Exp0
rhs_tc')]))
      (Subst
sbst, [], [])
      [(String, [(Var, Ty0)], Exp0)]
brs
  let ([Ty0]
as,[Ty0]
bs) = [(Ty0, Ty0)] -> ([Ty0], [Ty0])
forall a b. [(a, b)] -> ([a], [b])
unzip ([Ty0] -> [(Ty0, Ty0)]
forall a. [a] -> [(a, a)]
pairs [Ty0]
tys)
  Subst
s2 <- Exp0 -> [Ty0] -> [Ty0] -> TcM Subst
unifyl Exp0
ex [Ty0]
as [Ty0]
bs
  let s3 :: Subst
s3 = Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2
      tys' :: [Ty0]
tys' = (Ty0 -> Ty0) -> [Ty0] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Ty0 -> Ty0
zonkTy Subst
s3) [Ty0]
tys
  ((Ty0, Ty0) -> TcM ()) -> [(Ty0, Ty0)] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Ty0
a,Ty0
b) -> Exp0 -> Ty0 -> Ty0 -> TcM ()
ensureEqualTy Exp0
ex Ty0
a Ty0
b) ([Ty0] -> [(Ty0, Ty0)]
forall a. [a] -> [(a, a)]
pairs [Ty0]
tys')
  (Subst, Ty0, [(String, [(Var, Ty0)], Exp0)])
-> TcM (Subst, Ty0, [(String, [(Var, Ty0)], Exp0)])
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s3, [Ty0] -> Ty0
forall a. HasCallStack => [a] -> a
head [Ty0]
tys',[(String, [(Var, Ty0)], Exp0)]
exps)
  where
    -- pairs [1,2,3,4,5] = [(1,2), (2,3) (4,5)]
    pairs :: [a] -> [(a,a)]
    pairs :: forall a. [a] -> [(a, a)]
pairs []  = []
    pairs [a
_] = []
    pairs (a
x:a
y:[a]
xs) = (a
x,a
y) (a, a) -> [(a, a)] -> [(a, a)]
forall a. a -> [a] -> [a]
: [a] -> [(a, a)]
forall a. [a] -> [(a, a)]
pairs (a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs)

-- | Instantiate the topmost for-alls of the argument type with meta
-- type variables.
instantiate :: TyScheme -> TcM ([Ty0], Ty0)
instantiate :: TyScheme -> TcM ([Ty0], Ty0)
instantiate (ForAll [TyVar]
tvs Ty0
ty) = do
  [Ty0]
tvs' <- (TyVar -> TcM Ty0) -> [TyVar] -> TcM [Ty0]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (TcM Ty0 -> TyVar -> TcM Ty0
forall a b. a -> b -> a
const TcM Ty0
forall (m :: * -> *). MonadState Int m => m Ty0
newMetaTy) [TyVar]
tvs
  let ty' :: Ty0
ty' = Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar ([(TyVar, Ty0)] -> Map TyVar Ty0
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(TyVar, Ty0)] -> Map TyVar Ty0)
-> [(TyVar, Ty0)] -> Map TyVar Ty0
forall a b. (a -> b) -> a -> b
$ [TyVar] -> [Ty0] -> [(TyVar, Ty0)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TyVar]
tvs [Ty0]
tvs') Ty0
ty
  ([Ty0], Ty0) -> TcM ([Ty0], Ty0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Ty0]
tvs', Ty0
ty')

generalize :: Gamma -> Subst -> [TyVar] -> Ty0 -> TcM (Subst, TyScheme)
generalize :: Map Var TyScheme
-> Subst -> [TyVar] -> Ty0 -> TcM (Subst, TyScheme)
generalize Map Var TyScheme
env Subst
s [TyVar]
bound_tyvars Ty0
ty = do
  [TyVar]
new_bndrs <- (MetaTv -> TcM TyVar) -> [MetaTv] -> TcM [TyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM
                 (\(Meta Int
i) -> do
                       Var
v' <- Var -> Var -> Var
varAppend (Var -> Var -> Var) -> TcM Var -> TcM (Var -> Var)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcM Var
forall (m :: * -> *). MonadState Int m => m Var
genLetter TcM (Var -> Var) -> TcM Var -> TcM Var
forall a b. TcM (a -> b) -> TcM a -> TcM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Var -> TcM Var
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Var
toVar (String -> Var) -> String -> Var
forall a b. (a -> b) -> a -> b
$ String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)
                       TyVar -> TcM TyVar
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyVar -> TcM TyVar) -> TyVar -> TcM TyVar
forall a b. (a -> b) -> a -> b
$ Var -> TyVar
BoundTv Var
v')
                 [MetaTv]
meta_tvs
  let s2 :: Subst
s2  = Map MetaTv Ty0 -> Subst
Subst (Map MetaTv Ty0 -> Subst) -> Map MetaTv Ty0 -> Subst
forall a b. (a -> b) -> a -> b
$ [(MetaTv, Ty0)] -> Map MetaTv Ty0
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([MetaTv] -> [Ty0] -> [(MetaTv, Ty0)]
forall a b. [a] -> [b] -> [(a, b)]
zip [MetaTv]
meta_tvs ((TyVar -> Ty0) -> [TyVar] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map TyVar -> Ty0
TyVar [TyVar]
new_bndrs))
      ty' :: Ty0
ty' = Subst -> Ty0 -> Ty0
zonkTy (Subst
s Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2) Ty0
ty

      -- Generalize over BoundTv's too.
      free_tvs :: [TyVar]
free_tvs = (Ty0 -> [TyVar]
tyVarsInTy Ty0
ty) [TyVar] -> [TyVar] -> [TyVar]
forall a. Eq a => [a] -> [a] -> [a]
L.\\ [TyVar]
bound_tyvars
  (Subst, TyScheme) -> TcM (Subst, TyScheme)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2, [TyVar] -> Ty0 -> TyScheme
ForAll ([TyVar]
new_bndrs [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ [TyVar]
free_tvs) Ty0
ty')
  where
    env_tvs :: [MetaTv]
env_tvs = [TyScheme] -> [MetaTv]
metaTvsInTySchemes (Map Var TyScheme -> [TyScheme]
forall k a. Map k a -> [a]
M.elems Map Var TyScheme
env)
    res_tvs :: [MetaTv]
res_tvs = Ty0 -> [MetaTv]
metaTvsInTy Ty0
ty

    meta_tvs :: [MetaTv]
    meta_tvs :: [MetaTv]
meta_tvs = [MetaTv]
res_tvs [MetaTv] -> [MetaTv] -> [MetaTv]
forall a. Eq a => [a] -> [a] -> [a]
L.\\ [MetaTv]
env_tvs

--
instDataConTy :: DDefs0 -> DataCon -> TcM ([Ty0], [Ty0], Ty0)
instDataConTy :: DDefs0 -> String -> TcM ([Ty0], [Ty0], Ty0)
instDataConTy DDefs0
ddefs String
dcon = do
  let tycon :: String
tycon = DDefs0 -> String -> String
forall a. Out a => DDefs a -> String -> String
getTyOfDataCon DDefs0
ddefs String
dcon
      ddf :: DDef Ty0
ddf   = DDefs0 -> String -> DDef Ty0
forall a. Out a => DDefs a -> String -> DDef a
lookupDDef DDefs0
ddefs String
tycon
      arg_tys :: [Ty0]
arg_tys = DDefs0 -> String -> [Ty0]
forall a. Out a => DDefs a -> String -> [a]
lookupDataCon DDefs0
ddefs String
dcon
      tyvars :: [TyVar]
tyvars  = [Ty0] -> [TyVar]
tyVarsInTys [Ty0]
arg_tys
  -- Given a datatype;
  --
  --     data Either a b = Left a | Right b
  --
  -- and some constructor, build a substituion;
  --
  --     Left  [c] => [ a -> c    , b -> fresh ]
  --     Right [c] => [ a -> fresh, b -> c     ]
  --
  [Ty0]
tyArgs' <- (TyVar -> TcM Ty0) -> [TyVar] -> TcM [Ty0]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\TyVar
tyarg ->
                if TyVar
tyarg TyVar -> [TyVar] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TyVar]
tyvars
                then Ty0 -> TcM Ty0
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyVar -> Ty0
TyVar TyVar
tyarg)
                else TcM Ty0
forall (m :: * -> *). MonadState Int m => m Ty0
newMetaTy)
             (DDef Ty0 -> [TyVar]
forall a. DDef a -> [TyVar]
tyArgs DDef Ty0
ddf)
  (Map TyVar Ty0
env1, [Ty0]
tyArgs'') <- [Ty0] -> TcM (Map TyVar Ty0, [Ty0])
tyVarToMetaTyl [Ty0]
tyArgs'
  (Map TyVar Ty0
_env2, [Ty0]
arg_tys_inst) <- [Ty0] -> TcM (Map TyVar Ty0, [Ty0])
tyVarToMetaTyl ((Ty0 -> Ty0) -> [Ty0] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
env1) [Ty0]
arg_tys)
  let ret_ty_inst :: Ty0
ret_ty_inst = String -> [Ty0] -> Ty0
PackedTy String
tycon [Ty0]
tyArgs''
  ([Ty0], [Ty0], Ty0) -> TcM ([Ty0], [Ty0], Ty0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Ty0]
tyArgs'', [Ty0]
arg_tys_inst, Ty0
ret_ty_inst)


--------------------------------------------------------------------------------
-- Type environment
--------------------------------------------------------------------------------

-- We can't directly use Env2 because of the way it's tied together with
-- PreExp and the Expression class. We want to annotate L0 expressions
-- with 'Ty0' but Gamma should store 'TyScheme's.
type Gamma = TyEnv TyScheme

instance FreeVars a => FreeVars (TyEnv a) where
  gFreeVars :: TyEnv a -> Set Var
gFreeVars TyEnv a
env = (a -> Set Var -> Set Var) -> Set Var -> [a] -> Set Var
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
S.union (Set Var -> Set Var -> Set Var)
-> (a -> Set Var) -> a -> Set Var -> Set Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Set Var
forall a. FreeVars a => a -> Set Var
gFreeVars) Set Var
forall a. Set a
S.empty (TyEnv a -> [a]
forall k a. Map k a -> [a]
M.elems TyEnv a
env)

--------------------------------------------------------------------------------
-- Substitution
--------------------------------------------------------------------------------

newtype Subst = Subst (M.Map MetaTv Ty0)
  deriving (Eq Subst
Eq Subst
-> (Subst -> Subst -> Ordering)
-> (Subst -> Subst -> Bool)
-> (Subst -> Subst -> Bool)
-> (Subst -> Subst -> Bool)
-> (Subst -> Subst -> Bool)
-> (Subst -> Subst -> Subst)
-> (Subst -> Subst -> Subst)
-> Ord Subst
Subst -> Subst -> Bool
Subst -> Subst -> Ordering
Subst -> Subst -> Subst
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Subst -> Subst -> Ordering
compare :: Subst -> Subst -> Ordering
$c< :: Subst -> Subst -> Bool
< :: Subst -> Subst -> Bool
$c<= :: Subst -> Subst -> Bool
<= :: Subst -> Subst -> Bool
$c> :: Subst -> Subst -> Bool
> :: Subst -> Subst -> Bool
$c>= :: Subst -> Subst -> Bool
>= :: Subst -> Subst -> Bool
$cmax :: Subst -> Subst -> Subst
max :: Subst -> Subst -> Subst
$cmin :: Subst -> Subst -> Subst
min :: Subst -> Subst -> Subst
Ord, Subst -> Subst -> Bool
(Subst -> Subst -> Bool) -> (Subst -> Subst -> Bool) -> Eq Subst
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Subst -> Subst -> Bool
== :: Subst -> Subst -> Bool
$c/= :: Subst -> Subst -> Bool
/= :: Subst -> Subst -> Bool
Eq, ReadPrec [Subst]
ReadPrec Subst
Int -> ReadS Subst
ReadS [Subst]
(Int -> ReadS Subst)
-> ReadS [Subst]
-> ReadPrec Subst
-> ReadPrec [Subst]
-> Read Subst
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS Subst
readsPrec :: Int -> ReadS Subst
$creadList :: ReadS [Subst]
readList :: ReadS [Subst]
$creadPrec :: ReadPrec Subst
readPrec :: ReadPrec Subst
$creadListPrec :: ReadPrec [Subst]
readListPrec :: ReadPrec [Subst]
Read, Int -> Subst -> String -> String
[Subst] -> String -> String
Subst -> String
(Int -> Subst -> String -> String)
-> (Subst -> String) -> ([Subst] -> String -> String) -> Show Subst
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Subst -> String -> String
showsPrec :: Int -> Subst -> String -> String
$cshow :: Subst -> String
show :: Subst -> String
$cshowList :: [Subst] -> String -> String
showList :: [Subst] -> String -> String
Show, (forall x. Subst -> Rep Subst x)
-> (forall x. Rep Subst x -> Subst) -> Generic Subst
forall x. Rep Subst x -> Subst
forall x. Subst -> Rep Subst x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Subst -> Rep Subst x
from :: forall x. Subst -> Rep Subst x
$cto :: forall x. Rep Subst x -> Subst
to :: forall x. Rep Subst x -> Subst
Generic, Int -> Subst -> Doc
[Subst] -> Doc
Subst -> Doc
(Int -> Subst -> Doc)
-> (Subst -> Doc) -> ([Subst] -> Doc) -> Out Subst
forall a. (Int -> a -> Doc) -> (a -> Doc) -> ([a] -> Doc) -> Out a
$cdocPrec :: Int -> Subst -> Doc
docPrec :: Int -> Subst -> Doc
$cdoc :: Subst -> Doc
doc :: Subst -> Doc
$cdocList :: [Subst] -> Doc
docList :: [Subst] -> Doc
Out)

instance Semigroup Subst where
  -- (Subst s1) <> (Subst s2) =
  --   let mp = M.map (zonkTy (Subst s1)) s2 `M.union` s1 in Subst mp
  (<>) :: Subst -> Subst -> Subst
  (Subst Map MetaTv Ty0
s1) <> :: Subst -> Subst -> Subst
<> (Subst Map MetaTv Ty0
s2) =
    let s2' :: Map MetaTv Ty0
s2' = (Ty0 -> Ty0) -> Map MetaTv Ty0 -> Map MetaTv Ty0
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (Subst -> Ty0 -> Ty0
zonkTy (Map MetaTv Ty0 -> Subst
Subst Map MetaTv Ty0
s1)) Map MetaTv Ty0
s2
        mp :: Map MetaTv Ty0
mp =  (Ty0 -> Ty0 -> Ty0)
-> Map MetaTv Ty0 -> Map MetaTv Ty0 -> Map MetaTv Ty0
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Ty0 -> Ty0 -> Ty0
combine Map MetaTv Ty0
s2' Map MetaTv Ty0
s1
    in Map MetaTv Ty0 -> Subst
Subst Map MetaTv Ty0
mp

-- | Combine substitutions. In case of substitutions with intersecting keys,
-- we will take the narrower type of the two. e.g. combine [($1, $2)] [($1, IntTy)]
-- should be [($1, IntTy)]. Map.union does a left biased union so it will result in [($1, $2)]
combine :: Ty0 -> Ty0 -> Ty0
combine :: Ty0 -> Ty0 -> Ty0
combine Ty0
v1 Ty0
v2 | Ty0
v1 Ty0 -> Ty0 -> Bool
forall a. Eq a => a -> a -> Bool
== Ty0
v2 = Ty0
v1
              | Bool
otherwise = case (Ty0
v1, Ty0
v2) of
                (MetaTv MetaTv
_, Ty0
_) -> Ty0
v2
                (Ty0
_, MetaTv MetaTv
_) -> Ty0
v1
                (ArrowTy [Ty0]
xs Ty0
y, ArrowTy [Ty0]
xs' Ty0
y') -> [Ty0] -> Ty0 -> Ty0
ArrowTy ((Ty0 -> Ty0 -> Ty0) -> [Ty0] -> [Ty0] -> [Ty0]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Ty0 -> Ty0 -> Ty0
combine [Ty0]
xs [Ty0]
xs') (Ty0 -> Ty0 -> Ty0
combine Ty0
y Ty0
y')
                (VectorTy Ty0
v1', VectorTy Ty0
v2') -> Ty0 -> Ty0
VectorTy (Ty0 -> Ty0) -> Ty0 -> Ty0
forall a b. (a -> b) -> a -> b
$ Ty0 -> Ty0 -> Ty0
combine Ty0
v1' Ty0
v2'
                (ProdTy [Ty0]
v1s, ProdTy [Ty0]
v2s) -> [Ty0] -> Ty0
ProdTy ((Ty0 -> Ty0 -> Ty0) -> [Ty0] -> [Ty0] -> [Ty0]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Ty0 -> Ty0 -> Ty0
combine [Ty0]
v1s [Ty0]
v2s)
                (PackedTy String
a1 [Ty0]
v1s, PackedTy String
a2 [Ty0]
v2s) ->
                  if String
a1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
a2 then String -> [Ty0] -> Ty0
PackedTy String
a1 ((Ty0 -> Ty0 -> Ty0) -> [Ty0] -> [Ty0] -> [Ty0]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Ty0 -> Ty0 -> Ty0
combine [Ty0]
v1s [Ty0]
v2s)
                  else String -> Ty0
forall a. HasCallStack => String -> a
error (String -> Ty0) -> String -> Ty0
forall a b. (a -> b) -> a -> b
$ String
"PackedTy doesn't match "String -> String -> String
forall a. [a] -> [a] -> [a]
++ Ty0 -> String
forall a. Out a => a -> String
sdoc Ty0
v1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" with " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Ty0 -> String
forall a. Out a => a -> String
sdoc Ty0
v2
                (Ty0, Ty0)
_ -> String -> Ty0
forall a. HasCallStack => String -> a
error (String -> Ty0) -> String -> Ty0
forall a b. (a -> b) -> a -> b
$ String
"Failed to combine = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Ty0 -> String
forall a. Out a => a -> String
sdoc Ty0
v1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" with " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Ty0 -> String
forall a. Out a => a -> String
sdoc Ty0
v2


emptySubst :: Subst
emptySubst :: Subst
emptySubst = Map MetaTv Ty0 -> Subst
Subst (Map MetaTv Ty0
forall k a. Map k a
M.empty)

-- | Perform substitutions in the type.
zonkTy :: Subst -> Ty0 -> Ty0
zonkTy :: Subst -> Ty0 -> Ty0
zonkTy s :: Subst
s@(Subst Map MetaTv Ty0
mp) Ty0
ty =
  case Ty0
ty of
    Ty0
IntTy   -> Ty0
ty
    Ty0
CharTy  -> Ty0
ty
    Ty0
FloatTy -> Ty0
ty
    Ty0
SymTy0  -> Ty0
ty
    Ty0
BoolTy  -> Ty0
ty
    TyVar{} -> Ty0
ty
    MetaTv MetaTv
v -> case MetaTv -> Map MetaTv Ty0 -> Maybe Ty0
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup MetaTv
v Map MetaTv Ty0
mp of
                  Maybe Ty0
Nothing -> MetaTv -> Ty0
MetaTv MetaTv
v
                  Just t :: Ty0
t@(MetaTv MetaTv
w) -> if MetaTv
v MetaTv -> MetaTv -> Bool
forall a. Eq a => a -> a -> Bool
== MetaTv
w then MetaTv -> Ty0
MetaTv MetaTv
v else Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
t
                  Just Ty0
t -> Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
t
    ProdTy [Ty0]
tys  -> [Ty0] -> Ty0
ProdTy ((Ty0 -> Ty0) -> [Ty0] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map Ty0 -> Ty0
go [Ty0]
tys)
    SymDictTy Maybe Var
v Ty0
t -> Maybe Var -> Ty0 -> Ty0
SymDictTy Maybe Var
v (Ty0 -> Ty0
go Ty0
t)
    PDictTy Ty0
k Ty0
v -> Ty0 -> Ty0 -> Ty0
PDictTy (Ty0 -> Ty0
go Ty0
k) (Ty0 -> Ty0
go Ty0
v)
    ArrowTy [Ty0]
tys Ty0
b  -> [Ty0] -> Ty0 -> Ty0
ArrowTy ((Ty0 -> Ty0) -> [Ty0] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map Ty0 -> Ty0
go [Ty0]
tys) (Ty0 -> Ty0
go Ty0
b)
    PackedTy String
t [Ty0]
tys -> String -> [Ty0] -> Ty0
PackedTy String
t ((Ty0 -> Ty0) -> [Ty0] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map Ty0 -> Ty0
go [Ty0]
tys)
    VectorTy Ty0
t -> Ty0 -> Ty0
VectorTy (Ty0 -> Ty0
go Ty0
t)
    ListTy Ty0
t -> Ty0 -> Ty0
ListTy (Ty0 -> Ty0
go Ty0
t)
    Ty0
ArenaTy  -> Ty0
ty
    Ty0
SymSetTy -> Ty0
ty
    Ty0
SymHashTy -> Ty0
ty
    Ty0
IntHashTy -> Ty0
ty
  where
    go :: Ty0 -> Ty0
go = Subst -> Ty0 -> Ty0
zonkTy Subst
s

zonkTyScheme :: Subst -> TyScheme -> TyScheme
zonkTyScheme :: Subst -> TyScheme -> TyScheme
zonkTyScheme Subst
s (ForAll [TyVar]
tvs Ty0
ty) = [TyVar] -> Ty0 -> TyScheme
ForAll [TyVar]
tvs (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty)

zonkTyEnv :: Subst -> Gamma -> Gamma
zonkTyEnv :: Subst -> Map Var TyScheme -> Map Var TyScheme
zonkTyEnv Subst
s Map Var TyScheme
env = (TyScheme -> TyScheme) -> Map Var TyScheme -> Map Var TyScheme
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (Subst -> TyScheme -> TyScheme
zonkTyScheme Subst
s) Map Var TyScheme
env

-- Apply a substitution to an expression i.e substitue all types in it.
zonkExp :: Subst -> Exp0 -> Exp0
zonkExp :: Subst -> Exp0 -> Exp0
zonkExp Subst
s Exp0
ex =
  case Exp0
ex of
    VarE{}    -> Exp0
ex
    LitE{}    -> Exp0
ex
    CharE{}   -> Exp0
ex
    FloatE{}  -> Exp0
ex
    LitSymE{} -> Exp0
ex
    AppE Var
f [Ty0]
tyapps [Exp0]
args -> let tyapps1 :: [Ty0]
tyapps1 = (Ty0 -> Ty0) -> [Ty0] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Ty0 -> Ty0
zonkTy Subst
s) [Ty0]
tyapps
                          in Var -> [Ty0] -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Var -> [loc] -> [PreExp ext loc dec] -> PreExp ext loc dec
AppE Var
f [Ty0]
tyapps1 ((Exp0 -> Exp0) -> [Exp0] -> [Exp0]
forall a b. (a -> b) -> [a] -> [b]
map Exp0 -> Exp0
go [Exp0]
args)
    PrimAppE Prim Ty0
pr [Exp0]
args  ->
      let pr' :: Prim Ty0
pr' = case Prim Ty0
pr of
                  VAllocP  Ty0
ty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
VAllocP  (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty)
                  VFreeP  Ty0
ty  -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
VFreeP  (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty)
                  VFree2P  Ty0
ty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
VFree2P  (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty)
                  VLengthP Ty0
ty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
VLengthP (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty)
                  VNthP    Ty0
ty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
VNthP    (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty)
                  VSliceP  Ty0
ty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
VSliceP  (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty)
                  VConcatP Ty0
ty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
VConcatP (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty)
                  InplaceVUpdateP Ty0
ty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
InplaceVUpdateP (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty)
                  VSortP   Ty0
ty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
VSortP   (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty)
                  VMergeP Ty0
ty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
VMergeP (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty)
                  PDictAllocP Ty0
k Ty0
v -> Ty0 -> Ty0 -> Prim Ty0
forall ty. ty -> ty -> Prim ty
PDictAllocP (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
k) (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
v)
                  PDictInsertP Ty0
k Ty0
v -> Ty0 -> Ty0 -> Prim Ty0
forall ty. ty -> ty -> Prim ty
PDictInsertP (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
k) (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
v)
                  PDictLookupP Ty0
k Ty0
v -> Ty0 -> Ty0 -> Prim Ty0
forall ty. ty -> ty -> Prim ty
PDictLookupP (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
k) (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
v)
                  PDictHasKeyP Ty0
k Ty0
v -> Ty0 -> Ty0 -> Prim Ty0
forall ty. ty -> ty -> Prim ty
PDictHasKeyP (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
k) (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
v)
                  PDictForkP Ty0
k Ty0
v -> Ty0 -> Ty0 -> Prim Ty0
forall ty. ty -> ty -> Prim ty
PDictForkP (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
k) (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
v)
                  PDictJoinP Ty0
k Ty0
v -> Ty0 -> Ty0 -> Prim Ty0
forall ty. ty -> ty -> Prim ty
PDictJoinP (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
k) (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
v)
                  LLAllocP Ty0
ty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
LLAllocP (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty)
                  LLIsEmptyP Ty0
ty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
LLIsEmptyP (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty)
                  LLConsP Ty0
ty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
LLConsP (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty)
                  LLHeadP Ty0
ty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
LLHeadP (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty)
                  LLTailP Ty0
ty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
LLTailP (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty)
                  LLFreeP Ty0
ty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
LLFreeP (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty)
                  LLFree2P Ty0
ty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
LLFree2P (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty)
                  LLCopyP Ty0
ty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
LLCopyP (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty)
                  InplaceVSortP Ty0
ty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
InplaceVSortP (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty)
                  ReadArrayFile Maybe (String, Int)
fp Ty0
ty -> Maybe (String, Int) -> Ty0 -> Prim Ty0
forall ty. Maybe (String, Int) -> ty -> Prim ty
ReadArrayFile Maybe (String, Int)
fp (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty)
                  Prim Ty0
_ -> Prim Ty0
pr
      in Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty0
pr' ((Exp0 -> Exp0) -> [Exp0] -> [Exp0]
forall a b. (a -> b) -> [a] -> [b]
map Exp0 -> Exp0
go [Exp0]
args)
    -- Let doesn't store any tyapps.
    LetE (Var
v,[Ty0]
tyapps,Ty0
ty,Exp0
rhs) Exp0
bod -> (Var, [Ty0], Ty0, Exp0) -> Exp0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
(Var, [loc], dec, PreExp ext loc dec)
-> PreExp ext loc dec -> PreExp ext loc dec
LetE (Var
v, [Ty0]
tyapps, Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty, Exp0 -> Exp0
go Exp0
rhs) (Exp0 -> Exp0
go Exp0
bod)
    IfE Exp0
a Exp0
b Exp0
c  -> Exp0 -> Exp0 -> Exp0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
PreExp ext loc dec
-> PreExp ext loc dec -> PreExp ext loc dec -> PreExp ext loc dec
IfE (Exp0 -> Exp0
go Exp0
a) (Exp0 -> Exp0
go Exp0
b) (Exp0 -> Exp0
go Exp0
c)
    MkProdE [Exp0]
ls -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
[PreExp ext loc dec] -> PreExp ext loc dec
MkProdE ((Exp0 -> Exp0) -> [Exp0] -> [Exp0]
forall a b. (a -> b) -> [a] -> [b]
map Exp0 -> Exp0
go [Exp0]
ls)
    ProjE Int
i Exp0
e  -> Int -> Exp0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
Int -> PreExp ext loc dec -> PreExp ext loc dec
ProjE Int
i (Exp0 -> Exp0
go Exp0
e)
    CaseE Exp0
scrt [(String, [(Var, Ty0)], Exp0)]
brs ->
      Exp0 -> [(String, [(Var, Ty0)], Exp0)] -> Exp0
forall (ext :: * -> * -> *) loc dec.
PreExp ext loc dec
-> [(String, [(Var, loc)], PreExp ext loc dec)]
-> PreExp ext loc dec
CaseE (Exp0 -> Exp0
go Exp0
scrt) (((String, [(Var, Ty0)], Exp0) -> (String, [(Var, Ty0)], Exp0))
-> [(String, [(Var, Ty0)], Exp0)] -> [(String, [(Var, Ty0)], Exp0)]
forall a b. (a -> b) -> [a] -> [b]
map
                        (\(String
dcon,[(Var, Ty0)]
vtys,Exp0
rhs) -> let ([Var]
vars,[Ty0]
tys) = [(Var, Ty0)] -> ([Var], [Ty0])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Var, Ty0)]
vtys
                                                 vtys' :: [(Var, Ty0)]
vtys' = [Var] -> [Ty0] -> [(Var, Ty0)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
vars ([Ty0] -> [(Var, Ty0)]) -> [Ty0] -> [(Var, Ty0)]
forall a b. (a -> b) -> a -> b
$ (Ty0 -> Ty0) -> [Ty0] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Ty0 -> Ty0
zonkTy Subst
s) [Ty0]
tys
                                             in (String
dcon, [(Var, Ty0)]
vtys', Exp0 -> Exp0
go Exp0
rhs))
                        [(String, [(Var, Ty0)], Exp0)]
brs)
    DataConE (ProdTy [Ty0]
tyapps) String
dcon [Exp0]
args ->
      Ty0 -> String -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
loc -> String -> [PreExp ext loc dec] -> PreExp ext loc dec
DataConE ([Ty0] -> Ty0
ProdTy ((Ty0 -> Ty0) -> [Ty0] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Ty0 -> Ty0
zonkTy Subst
s) [Ty0]
tyapps)) String
dcon ((Exp0 -> Exp0) -> [Exp0] -> [Exp0]
forall a b. (a -> b) -> [a] -> [b]
map Exp0 -> Exp0
go [Exp0]
args)
    DataConE{} -> String -> Exp0
forall a. HasCallStack => String -> a
error (String -> Exp0) -> String -> Exp0
forall a b. (a -> b) -> a -> b
$ String
"zonkExp: Expected (ProdTy tyapps), got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Exp0 -> String
forall a. Out a => a -> String
sdoc Exp0
ex
    TimeIt Exp0
e Ty0
ty Bool
b -> Exp0 -> Ty0 -> Bool -> Exp0
forall (ext :: * -> * -> *) loc dec.
PreExp ext loc dec -> dec -> Bool -> PreExp ext loc dec
TimeIt (Exp0 -> Exp0
go Exp0
e) (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty) Bool
b
    WithArenaE Var
v Exp0
e -> Var -> Exp0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
Var -> PreExp ext loc dec -> PreExp ext loc dec
WithArenaE Var
v (Exp0 -> Exp0
go Exp0
e)
    Ext (LambdaE [(Var, Ty0)]
args Exp0
bod) -> E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext ([(Var, Ty0)] -> Exp0 -> E0Ext Ty0 Ty0
forall loc dec.
[(Var, dec)] -> PreExp E0Ext loc dec -> E0Ext loc dec
LambdaE (((Var, Ty0) -> (Var, Ty0)) -> [(Var, Ty0)] -> [(Var, Ty0)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Var
v,Ty0
ty) -> (Var
v, Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty)) [(Var, Ty0)]
args) (Exp0 -> Exp0
go Exp0
bod))
    Ext (PolyAppE Exp0
rator Exp0
rand) -> E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext (Exp0 -> Exp0 -> E0Ext Ty0 Ty0
forall loc dec.
PreExp E0Ext loc dec -> PreExp E0Ext loc dec -> E0Ext loc dec
PolyAppE (Exp0 -> Exp0
go Exp0
rator) (Exp0 -> Exp0
go Exp0
rand))
    Ext (FunRefE [Ty0]
tyapps Var
f)    -> let tyapps1 :: [Ty0]
tyapps1 = (Ty0 -> Ty0) -> [Ty0] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Ty0 -> Ty0
zonkTy Subst
s) [Ty0]
tyapps
                                 in E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext ([Ty0] -> Var -> E0Ext Ty0 Ty0
forall loc dec. [loc] -> Var -> E0Ext loc dec
FunRefE [Ty0]
tyapps1 Var
f)
    Ext (BenchE Var
fn [Ty0]
tyapps [Exp0]
args Bool
b) -> let tyapps1 :: [Ty0]
tyapps1 = (Ty0 -> Ty0) -> [Ty0] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Ty0 -> Ty0
zonkTy Subst
s) [Ty0]
tyapps
                                     in E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext (Var -> [Ty0] -> [Exp0] -> Bool -> E0Ext Ty0 Ty0
forall loc dec.
Var -> [loc] -> [PreExp E0Ext loc dec] -> Bool -> E0Ext loc dec
BenchE Var
fn [Ty0]
tyapps1 ((Exp0 -> Exp0) -> [Exp0] -> [Exp0]
forall a b. (a -> b) -> [a] -> [b]
map Exp0 -> Exp0
go [Exp0]
args) Bool
b)
    Ext (ParE0 [Exp0]
ls) -> E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext (E0Ext Ty0 Ty0 -> Exp0) -> E0Ext Ty0 Ty0 -> Exp0
forall a b. (a -> b) -> a -> b
$ [Exp0] -> E0Ext Ty0 Ty0
forall loc dec. [PreExp E0Ext loc dec] -> E0Ext loc dec
ParE0 ((Exp0 -> Exp0) -> [Exp0] -> [Exp0]
forall a b. (a -> b) -> [a] -> [b]
map Exp0 -> Exp0
go [Exp0]
ls)
    Ext (L Loc
p Exp0
e)    -> E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext (E0Ext Ty0 Ty0 -> Exp0) -> E0Ext Ty0 Ty0 -> Exp0
forall a b. (a -> b) -> a -> b
$ Loc -> Exp0 -> E0Ext Ty0 Ty0
forall loc dec. Loc -> PreExp E0Ext loc dec -> E0Ext loc dec
L Loc
p (Exp0 -> Exp0
go Exp0
e)
    Ext (PrintPacked Ty0
ty Exp0
arg) -> E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext (E0Ext Ty0 Ty0 -> Exp0) -> E0Ext Ty0 Ty0 -> Exp0
forall a b. (a -> b) -> a -> b
$ Ty0 -> Exp0 -> E0Ext Ty0 Ty0
forall loc dec. dec -> PreExp E0Ext loc dec -> E0Ext loc dec
PrintPacked (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty) (Exp0 -> Exp0
go Exp0
arg)
    Ext (CopyPacked Ty0
ty Exp0
arg) -> E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext (E0Ext Ty0 Ty0 -> Exp0) -> E0Ext Ty0 Ty0 -> Exp0
forall a b. (a -> b) -> a -> b
$ Ty0 -> Exp0 -> E0Ext Ty0 Ty0
forall loc dec. dec -> PreExp E0Ext loc dec -> E0Ext loc dec
CopyPacked (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty) (Exp0 -> Exp0
go Exp0
arg)
    Ext (TravPacked Ty0
ty Exp0
arg) -> E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext (E0Ext Ty0 Ty0 -> Exp0) -> E0Ext Ty0 Ty0 -> Exp0
forall a b. (a -> b) -> a -> b
$ Ty0 -> Exp0 -> E0Ext Ty0 Ty0
forall loc dec. dec -> PreExp E0Ext loc dec -> E0Ext loc dec
TravPacked (Subst -> Ty0 -> Ty0
zonkTy Subst
s Ty0
ty) (Exp0 -> Exp0
go Exp0
arg)
    Ext (LinearExt{}) -> String -> Exp0
forall a. HasCallStack => String -> a
error (String -> Exp0) -> String -> Exp0
forall a b. (a -> b) -> a -> b
$ String
"zonkExp: a linear types extension wasn't desugared: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Exp0 -> String
forall a. Out a => a -> String
sdoc Exp0
ex
    SpawnE Var
fn [Ty0]
tyapps [Exp0]
args -> let tyapps1 :: [Ty0]
tyapps1 = (Ty0 -> Ty0) -> [Ty0] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Ty0 -> Ty0
zonkTy Subst
s) [Ty0]
tyapps
                             in Var -> [Ty0] -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Var -> [loc] -> [PreExp ext loc dec] -> PreExp ext loc dec
SpawnE Var
fn [Ty0]
tyapps1 ((Exp0 -> Exp0) -> [Exp0] -> [Exp0]
forall a b. (a -> b) -> [a] -> [b]
map Exp0 -> Exp0
go [Exp0]
args)
    Exp0
SyncE    -> Exp0
forall (ext :: * -> * -> *) loc dec. PreExp ext loc dec
SyncE
    MapE{}   -> String -> Exp0
forall a. HasCallStack => String -> a
error (String -> Exp0) -> String -> Exp0
forall a b. (a -> b) -> a -> b
$ String
"zonkExp: TODO, " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Exp0 -> String
forall a. Out a => a -> String
sdoc Exp0
ex
    FoldE{}  -> String -> Exp0
forall a. HasCallStack => String -> a
error (String -> Exp0) -> String -> Exp0
forall a b. (a -> b) -> a -> b
$ String
"zonkExp: TODO, " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Exp0 -> String
forall a. Out a => a -> String
sdoc Exp0
ex
  where
    go :: Exp0 -> Exp0
go = Subst -> Exp0 -> Exp0
zonkExp Subst
s

-- Substitute tyvars with types in a ddef.
substTyVarDDef :: DDef0 -> [Ty0] -> TcM DDef0
substTyVarDDef :: DDef Ty0 -> [Ty0] -> TcM (DDef Ty0)
substTyVarDDef d :: DDef Ty0
d@DDef{[TyVar]
tyArgs :: forall a. DDef a -> [TyVar]
tyArgs :: [TyVar]
tyArgs,[(String, [(Bool, Ty0)])]
dataCons :: forall a. DDef a -> [(String, [(Bool, a)])]
dataCons :: [(String, [(Bool, Ty0)])]
dataCons} [Ty0]
tys =
  if [TyVar] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TyVar]
tyArgs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [Ty0] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ty0]
tys
  then Doc -> TcM (DDef Ty0)
forall a. Doc -> TcM a
err (Doc -> TcM (DDef Ty0)) -> Doc -> TcM (DDef Ty0)
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"substTyVarDDef: tyArgs don't match the tyapps, in "
               Doc -> Doc -> Doc
<+> [TyVar] -> Doc
forall a. Out a => a -> Doc
doc [TyVar]
tyArgs Doc -> Doc -> Doc
<+> String -> Doc
text String
", " Doc -> Doc -> Doc
<+> [Ty0] -> Doc
forall a. Out a => a -> Doc
doc [Ty0]
tys
  else do
    let mp :: Map TyVar Ty0
mp = [(TyVar, Ty0)] -> Map TyVar Ty0
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([TyVar] -> [Ty0] -> [(TyVar, Ty0)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TyVar]
tyArgs [Ty0]
tys)
        dcons' :: [(String, [(Bool, Ty0)])]
dcons' = ((String, [(Bool, Ty0)]) -> (String, [(Bool, Ty0)]))
-> [(String, [(Bool, Ty0)])] -> [(String, [(Bool, Ty0)])]
forall a b. (a -> b) -> [a] -> [b]
map
                   (\(String
dcon,[(Bool, Ty0)]
btys) ->
                      let ([Bool]
boxity, [Ty0]
tys1) = [(Bool, Ty0)] -> ([Bool], [Ty0])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Bool, Ty0)]
btys
                          tys1' :: [Ty0]
tys1' = (Ty0 -> Ty0) -> [Ty0] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp) [Ty0]
tys1
                      in (String
dcon, [Bool] -> [Ty0] -> [(Bool, Ty0)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Bool]
boxity [Ty0]
tys1'))
                   [(String, [(Bool, Ty0)])]
dataCons
        free_tyvars :: [TyVar]
free_tyvars =  (Ty0 -> [TyVar]) -> [Ty0] -> [TyVar]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Ty0 -> [TyVar]
tyVarsInTy (Map TyVar Ty0 -> [Ty0]
forall k a. Map k a -> [a]
M.elems Map TyVar Ty0
mp)
    DDef Ty0 -> TcM (DDef Ty0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DDef Ty0
d { tyArgs :: [TyVar]
tyArgs   = [TyVar]
free_tyvars
           , dataCons :: [(String, [(Bool, Ty0)])]
dataCons = [(String, [(Bool, Ty0)])]
dcons' }

-- Substitue all tyvars in an expression.
substTyVarExp :: M.Map TyVar Ty0 -> Exp0 -> Exp0
substTyVarExp :: Map TyVar Ty0 -> Exp0 -> Exp0
substTyVarExp Map TyVar Ty0
s Exp0
ex =
  case Exp0
ex of
    VarE{}    -> Exp0
ex
    LitE{}    -> Exp0
ex
    CharE{}   -> Exp0
ex
    FloatE{}  -> Exp0
ex
    LitSymE{} -> Exp0
ex
    AppE Var
f [Ty0]
tyapps [Exp0]
arg -> let tyapps1 :: [Ty0]
tyapps1 = (Ty0 -> Ty0) -> [Ty0] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
s) [Ty0]
tyapps
                         in Var -> [Ty0] -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Var -> [loc] -> [PreExp ext loc dec] -> PreExp ext loc dec
AppE Var
f [Ty0]
tyapps1 ((Exp0 -> Exp0) -> [Exp0] -> [Exp0]
forall a b. (a -> b) -> [a] -> [b]
map Exp0 -> Exp0
go [Exp0]
arg)
    PrimAppE Prim Ty0
pr [Exp0]
args  -> Prim Ty0 -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE (Map TyVar Ty0 -> Prim Ty0 -> Prim Ty0
substTyVarPrim Map TyVar Ty0
s Prim Ty0
pr) ((Exp0 -> Exp0) -> [Exp0] -> [Exp0]
forall a b. (a -> b) -> [a] -> [b]
map Exp0 -> Exp0
go [Exp0]
args)
    -- Let doesn't store any tyapps.
    LetE (Var
v,[Ty0]
tyapps,Ty0
ty,Exp0
rhs) Exp0
bod -> (Var, [Ty0], Ty0, Exp0) -> Exp0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
(Var, [loc], dec, PreExp ext loc dec)
-> PreExp ext loc dec -> PreExp ext loc dec
LetE (Var
v, [Ty0]
tyapps, Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
s Ty0
ty, Exp0 -> Exp0
go Exp0
rhs) (Exp0 -> Exp0
go Exp0
bod)
    IfE Exp0
a Exp0
b Exp0
c  -> Exp0 -> Exp0 -> Exp0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
PreExp ext loc dec
-> PreExp ext loc dec -> PreExp ext loc dec -> PreExp ext loc dec
IfE (Exp0 -> Exp0
go Exp0
a) (Exp0 -> Exp0
go Exp0
b) (Exp0 -> Exp0
go Exp0
c)
    MkProdE [Exp0]
ls -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
[PreExp ext loc dec] -> PreExp ext loc dec
MkProdE ((Exp0 -> Exp0) -> [Exp0] -> [Exp0]
forall a b. (a -> b) -> [a] -> [b]
map Exp0 -> Exp0
go [Exp0]
ls)
    ProjE Int
i Exp0
e  -> Int -> Exp0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
Int -> PreExp ext loc dec -> PreExp ext loc dec
ProjE Int
i (Exp0 -> Exp0
go Exp0
e)
    CaseE Exp0
scrt [(String, [(Var, Ty0)], Exp0)]
brs ->
      Exp0 -> [(String, [(Var, Ty0)], Exp0)] -> Exp0
forall (ext :: * -> * -> *) loc dec.
PreExp ext loc dec
-> [(String, [(Var, loc)], PreExp ext loc dec)]
-> PreExp ext loc dec
CaseE (Exp0 -> Exp0
go Exp0
scrt) (((String, [(Var, Ty0)], Exp0) -> (String, [(Var, Ty0)], Exp0))
-> [(String, [(Var, Ty0)], Exp0)] -> [(String, [(Var, Ty0)], Exp0)]
forall a b. (a -> b) -> [a] -> [b]
map
                        (\(String
dcon,[(Var, Ty0)]
vtys,Exp0
rhs) -> let ([Var]
vars,[Ty0]
tys) = [(Var, Ty0)] -> ([Var], [Ty0])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Var, Ty0)]
vtys
                                                 vtys' :: [(Var, Ty0)]
vtys' = [Var] -> [Ty0] -> [(Var, Ty0)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
vars ([Ty0] -> [(Var, Ty0)]) -> [Ty0] -> [(Var, Ty0)]
forall a b. (a -> b) -> a -> b
$ (Ty0 -> Ty0) -> [Ty0] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
s) [Ty0]
tys
                                             in (String
dcon, [(Var, Ty0)]
vtys', Exp0 -> Exp0
go Exp0
rhs))
                        [(String, [(Var, Ty0)], Exp0)]
brs)
    DataConE (ProdTy [Ty0]
tyapps) String
dcon [Exp0]
args ->
      Ty0 -> String -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
loc -> String -> [PreExp ext loc dec] -> PreExp ext loc dec
DataConE ([Ty0] -> Ty0
ProdTy ((Ty0 -> Ty0) -> [Ty0] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
s) [Ty0]
tyapps)) String
dcon ((Exp0 -> Exp0) -> [Exp0] -> [Exp0]
forall a b. (a -> b) -> [a] -> [b]
map Exp0 -> Exp0
go [Exp0]
args)
    DataConE{} -> String -> Exp0
forall a. HasCallStack => String -> a
error (String -> Exp0) -> String -> Exp0
forall a b. (a -> b) -> a -> b
$ String
"substTyVarExp: Expected (ProdTy tyapps), got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Exp0 -> String
forall a. Out a => a -> String
sdoc Exp0
ex
    TimeIt Exp0
e Ty0
ty Bool
b -> Exp0 -> Ty0 -> Bool -> Exp0
forall (ext :: * -> * -> *) loc dec.
PreExp ext loc dec -> dec -> Bool -> PreExp ext loc dec
TimeIt (Exp0 -> Exp0
go Exp0
e) (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
s Ty0
ty) Bool
b
    Ext (LambdaE [(Var, Ty0)]
args Exp0
bod) -> E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext ([(Var, Ty0)] -> Exp0 -> E0Ext Ty0 Ty0
forall loc dec.
[(Var, dec)] -> PreExp E0Ext loc dec -> E0Ext loc dec
LambdaE (((Var, Ty0) -> (Var, Ty0)) -> [(Var, Ty0)] -> [(Var, Ty0)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Var
v,Ty0
ty) -> (Var
v, Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
s Ty0
ty)) [(Var, Ty0)]
args) (Exp0 -> Exp0
go Exp0
bod))
    Ext (PolyAppE Exp0
rator Exp0
rand) -> E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext (Exp0 -> Exp0 -> E0Ext Ty0 Ty0
forall loc dec.
PreExp E0Ext loc dec -> PreExp E0Ext loc dec -> E0Ext loc dec
PolyAppE (Exp0 -> Exp0
go Exp0
rator) (Exp0 -> Exp0
go Exp0
rand))
    Ext (FunRefE [Ty0]
tyapps Var
f) -> let tyapps1 :: [Ty0]
tyapps1 = (Ty0 -> Ty0) -> [Ty0] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
s) [Ty0]
tyapps
                              in E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext (E0Ext Ty0 Ty0 -> Exp0) -> E0Ext Ty0 Ty0 -> Exp0
forall a b. (a -> b) -> a -> b
$ [Ty0] -> Var -> E0Ext Ty0 Ty0
forall loc dec. [loc] -> Var -> E0Ext loc dec
FunRefE [Ty0]
tyapps1 Var
f
    Ext (BenchE Var
fn [Ty0]
tyapps [Exp0]
args Bool
b) -> let tyapps1 :: [Ty0]
tyapps1 = (Ty0 -> Ty0) -> [Ty0] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
s) [Ty0]
tyapps
                                     in E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext (Var -> [Ty0] -> [Exp0] -> Bool -> E0Ext Ty0 Ty0
forall loc dec.
Var -> [loc] -> [PreExp E0Ext loc dec] -> Bool -> E0Ext loc dec
BenchE Var
fn [Ty0]
tyapps1 ((Exp0 -> Exp0) -> [Exp0] -> [Exp0]
forall a b. (a -> b) -> [a] -> [b]
map Exp0 -> Exp0
go [Exp0]
args) Bool
b)
    Ext (ParE0 [Exp0]
ls) -> E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext (E0Ext Ty0 Ty0 -> Exp0) -> E0Ext Ty0 Ty0 -> Exp0
forall a b. (a -> b) -> a -> b
$ [Exp0] -> E0Ext Ty0 Ty0
forall loc dec. [PreExp E0Ext loc dec] -> E0Ext loc dec
ParE0 ((Exp0 -> Exp0) -> [Exp0] -> [Exp0]
forall a b. (a -> b) -> [a] -> [b]
map Exp0 -> Exp0
go [Exp0]
ls)
    Ext (PrintPacked Ty0
ty Exp0
arg) -> E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext (E0Ext Ty0 Ty0 -> Exp0) -> E0Ext Ty0 Ty0 -> Exp0
forall a b. (a -> b) -> a -> b
$ Ty0 -> Exp0 -> E0Ext Ty0 Ty0
forall loc dec. dec -> PreExp E0Ext loc dec -> E0Ext loc dec
PrintPacked (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
s Ty0
ty) (Exp0 -> Exp0
go Exp0
arg)
    Ext (CopyPacked Ty0
ty Exp0
arg) -> E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext (E0Ext Ty0 Ty0 -> Exp0) -> E0Ext Ty0 Ty0 -> Exp0
forall a b. (a -> b) -> a -> b
$ Ty0 -> Exp0 -> E0Ext Ty0 Ty0
forall loc dec. dec -> PreExp E0Ext loc dec -> E0Ext loc dec
CopyPacked (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
s Ty0
ty) (Exp0 -> Exp0
go Exp0
arg)
    Ext (TravPacked Ty0
ty Exp0
arg) -> E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext (E0Ext Ty0 Ty0 -> Exp0) -> E0Ext Ty0 Ty0 -> Exp0
forall a b. (a -> b) -> a -> b
$ Ty0 -> Exp0 -> E0Ext Ty0 Ty0
forall loc dec. dec -> PreExp E0Ext loc dec -> E0Ext loc dec
TravPacked (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
s Ty0
ty) (Exp0 -> Exp0
go Exp0
arg)
    Ext (L Loc
p Exp0
e)    -> E0Ext Ty0 Ty0 -> Exp0
forall (ext :: * -> * -> *) loc dec.
ext loc dec -> PreExp ext loc dec
Ext (E0Ext Ty0 Ty0 -> Exp0) -> E0Ext Ty0 Ty0 -> Exp0
forall a b. (a -> b) -> a -> b
$ Loc -> Exp0 -> E0Ext Ty0 Ty0
forall loc dec. Loc -> PreExp E0Ext loc dec -> E0Ext loc dec
L Loc
p (Exp0 -> Exp0
go Exp0
e)
    Ext (LinearExt{}) -> String -> Exp0
forall a. HasCallStack => String -> a
error (String -> Exp0) -> String -> Exp0
forall a b. (a -> b) -> a -> b
$ String
"substTyVarExp: a linear types extension wasn't desugared: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Exp0 -> String
forall a. Out a => a -> String
sdoc Exp0
ex
    WithArenaE{} -> String -> Exp0
forall a. HasCallStack => String -> a
error String
"substTyVarExp: WithArenaE not handled."
    SpawnE Var
f [Ty0]
tyapps [Exp0]
arg -> let tyapps1 :: [Ty0]
tyapps1 = (Ty0 -> Ty0) -> [Ty0] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
s) [Ty0]
tyapps
                           in Var -> [Ty0] -> [Exp0] -> Exp0
forall (ext :: * -> * -> *) loc dec.
Var -> [loc] -> [PreExp ext loc dec] -> PreExp ext loc dec
SpawnE Var
f [Ty0]
tyapps1 ((Exp0 -> Exp0) -> [Exp0] -> [Exp0]
forall a b. (a -> b) -> [a] -> [b]
map Exp0 -> Exp0
go [Exp0]
arg)
    Exp0
SyncE    -> Exp0
forall (ext :: * -> * -> *) loc dec. PreExp ext loc dec
SyncE
    MapE{}   -> String -> Exp0
forall a. HasCallStack => String -> a
error (String -> Exp0) -> String -> Exp0
forall a b. (a -> b) -> a -> b
$ String
"substTyVarExp: TODO, " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Exp0 -> String
forall a. Out a => a -> String
sdoc Exp0
ex
    FoldE{}  -> String -> Exp0
forall a. HasCallStack => String -> a
error (String -> Exp0) -> String -> Exp0
forall a b. (a -> b) -> a -> b
$ String
"substTyVarExp: TODO, " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Exp0 -> String
forall a. Out a => a -> String
sdoc Exp0
ex
  where
    go :: Exp0 -> Exp0
go = Map TyVar Ty0 -> Exp0 -> Exp0
substTyVarExp Map TyVar Ty0
s

substTyVarPrim :: M.Map TyVar Ty0 -> Prim Ty0 -> Prim Ty0
substTyVarPrim :: Map TyVar Ty0 -> Prim Ty0 -> Prim Ty0
substTyVarPrim Map TyVar Ty0
mp Prim Ty0
pr =
    case Prim Ty0
pr of
        VAllocP Ty0
elty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
VAllocP (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
elty)
        VFreeP  Ty0
elty  -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
VFreeP  (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
elty)
        VFree2P  Ty0
elty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
VFree2P  (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
elty)
        VLengthP Ty0
elty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
VLengthP (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
elty)
        VNthP Ty0
elty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
VNthP (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
elty)
        VSliceP Ty0
elty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
VSliceP (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
elty)
        InplaceVUpdateP Ty0
elty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
InplaceVUpdateP (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
elty)
        VConcatP Ty0
elty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
VConcatP (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
elty)
        VSortP Ty0
elty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
VSortP (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
elty)
        InplaceVSortP Ty0
elty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
InplaceVSortP (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
elty)
        VMergeP Ty0
elty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
VMergeP (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
elty)
        PDictInsertP Ty0
kty Ty0
vty -> Ty0 -> Ty0 -> Prim Ty0
forall ty. ty -> ty -> Prim ty
PDictInsertP (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
kty) (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
vty)
        PDictLookupP Ty0
kty Ty0
vty -> Ty0 -> Ty0 -> Prim Ty0
forall ty. ty -> ty -> Prim ty
PDictLookupP (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
kty) (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
vty)
        PDictAllocP Ty0
kty Ty0
vty -> Ty0 -> Ty0 -> Prim Ty0
forall ty. ty -> ty -> Prim ty
PDictAllocP (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
kty) (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
vty)
        PDictHasKeyP Ty0
kty Ty0
vty -> Ty0 -> Ty0 -> Prim Ty0
forall ty. ty -> ty -> Prim ty
PDictHasKeyP (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
kty) (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
vty)
        PDictForkP Ty0
kty Ty0
vty -> Ty0 -> Ty0 -> Prim Ty0
forall ty. ty -> ty -> Prim ty
PDictForkP (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
kty) (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
vty)
        PDictJoinP Ty0
kty Ty0
vty -> Ty0 -> Ty0 -> Prim Ty0
forall ty. ty -> ty -> Prim ty
PDictJoinP (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
kty) (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
vty)
        LLAllocP Ty0
elty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
LLAllocP (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
elty)
        LLIsEmptyP Ty0
elty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
LLIsEmptyP (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
elty)
        LLConsP Ty0
elty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
LLConsP (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
elty)
        LLHeadP Ty0
elty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
LLHeadP (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
elty)
        LLTailP Ty0
elty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
LLTailP (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
elty)
        LLFreeP Ty0
elty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
LLFreeP (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
elty)
        LLFree2P Ty0
elty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
LLFree2P (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
elty)
        LLCopyP Ty0
elty -> Ty0 -> Prim Ty0
forall ty. ty -> Prim ty
LLCopyP (Map TyVar Ty0 -> Ty0 -> Ty0
substTyVar Map TyVar Ty0
mp Ty0
elty)
        Prim Ty0
_ -> Prim Ty0
pr


tyVarToMetaTyl :: [Ty0] -> TcM (M.Map TyVar Ty0, [Ty0])
tyVarToMetaTyl :: [Ty0] -> TcM (Map TyVar Ty0, [Ty0])
tyVarToMetaTyl [Ty0]
tys =
  ((Map TyVar Ty0, [Ty0]) -> Ty0 -> TcM (Map TyVar Ty0, [Ty0]))
-> (Map TyVar Ty0, [Ty0]) -> [Ty0] -> TcM (Map TyVar Ty0, [Ty0])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM
    (\(Map TyVar Ty0
env', [Ty0]
acc) Ty0
ty -> do
            (Map TyVar Ty0
env'', Ty0
ty') <- Ty0 -> TcM (Map TyVar Ty0, Ty0)
tyVarToMetaTy Ty0
ty
            (Map TyVar Ty0, [Ty0]) -> TcM (Map TyVar Ty0, [Ty0])
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map TyVar Ty0
env' Map TyVar Ty0 -> Map TyVar Ty0 -> Map TyVar Ty0
forall a. Semigroup a => a -> a -> a
<> Map TyVar Ty0
env'', [Ty0]
acc [Ty0] -> [Ty0] -> [Ty0]
forall a. [a] -> [a] -> [a]
++ [Ty0
ty']))
    (Map TyVar Ty0
forall k a. Map k a
M.empty, [])
    [Ty0]
tys

-- | Replace the specified quantified type variables by
-- given meta type variables.
tyVarToMetaTy :: Ty0 -> TcM (M.Map TyVar Ty0, Ty0)
tyVarToMetaTy :: Ty0 -> TcM (Map TyVar Ty0, Ty0)
tyVarToMetaTy = Map TyVar Ty0 -> Ty0 -> TcM (Map TyVar Ty0, Ty0)
go Map TyVar Ty0
forall k a. Map k a
M.empty
  where
    go :: M.Map TyVar Ty0 -> Ty0 -> TcM (M.Map TyVar Ty0, Ty0)
    go :: Map TyVar Ty0 -> Ty0 -> TcM (Map TyVar Ty0, Ty0)
go Map TyVar Ty0
env Ty0
ty =
     case Ty0
ty of
       Ty0
IntTy    -> (Map TyVar Ty0, Ty0) -> TcM (Map TyVar Ty0, Ty0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map TyVar Ty0
env, Ty0
ty)
       Ty0
CharTy   -> (Map TyVar Ty0, Ty0) -> TcM (Map TyVar Ty0, Ty0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map TyVar Ty0
env, Ty0
ty)
       Ty0
FloatTy  -> (Map TyVar Ty0, Ty0) -> TcM (Map TyVar Ty0, Ty0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map TyVar Ty0
env, Ty0
ty)
       Ty0
SymTy0   -> (Map TyVar Ty0, Ty0) -> TcM (Map TyVar Ty0, Ty0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map TyVar Ty0
env, Ty0
ty)
       Ty0
BoolTy   -> (Map TyVar Ty0, Ty0) -> TcM (Map TyVar Ty0, Ty0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map TyVar Ty0
env, Ty0
ty)
       TyVar TyVar
v  -> do Ty0
mty <- TcM Ty0
forall (m :: * -> *). MonadState Int m => m Ty0
newMetaTy
                      (Map TyVar Ty0, Ty0) -> TcM (Map TyVar Ty0, Ty0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyVar -> Ty0 -> Map TyVar Ty0 -> Map TyVar Ty0
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert TyVar
v Ty0
mty Map TyVar Ty0
env, Ty0
mty)
       MetaTv{} -> (Map TyVar Ty0, Ty0) -> TcM (Map TyVar Ty0, Ty0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map TyVar Ty0
env, Ty0
ty)
       ProdTy [Ty0]
tys -> do (Map TyVar Ty0
env', [Ty0]
tys') <- Map TyVar Ty0 -> [Ty0] -> TcM (Map TyVar Ty0, [Ty0])
gol Map TyVar Ty0
env [Ty0]
tys
                        (Map TyVar Ty0, Ty0) -> TcM (Map TyVar Ty0, Ty0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map TyVar Ty0
env', [Ty0] -> Ty0
ProdTy [Ty0]
tys')
       SymDictTy Maybe Var
v Ty0
t -> do (Map TyVar Ty0
env', Ty0
t') <- Map TyVar Ty0 -> Ty0 -> TcM (Map TyVar Ty0, Ty0)
go Map TyVar Ty0
env Ty0
t
                           (Map TyVar Ty0, Ty0) -> TcM (Map TyVar Ty0, Ty0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map TyVar Ty0
env', Maybe Var -> Ty0 -> Ty0
SymDictTy Maybe Var
v Ty0
t')
       PDictTy Ty0
k Ty0
v -> do (Map TyVar Ty0
env', Ty0
k') <- Map TyVar Ty0 -> Ty0 -> TcM (Map TyVar Ty0, Ty0)
go Map TyVar Ty0
env Ty0
k
                         (Map TyVar Ty0
env'', Ty0
v') <- Map TyVar Ty0 -> Ty0 -> TcM (Map TyVar Ty0, Ty0)
go Map TyVar Ty0
env' Ty0
v
                         (Map TyVar Ty0, Ty0) -> TcM (Map TyVar Ty0, Ty0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map TyVar Ty0
env'', Ty0 -> Ty0 -> Ty0
PDictTy Ty0
k' Ty0
v')
       ArrowTy [Ty0]
as Ty0
b -> do (Map TyVar Ty0
env', [Ty0]
as') <- Map TyVar Ty0 -> [Ty0] -> TcM (Map TyVar Ty0, [Ty0])
gol Map TyVar Ty0
env [Ty0]
as
                          (Map TyVar Ty0
env'', Ty0
b') <- Map TyVar Ty0 -> Ty0 -> TcM (Map TyVar Ty0, Ty0)
go Map TyVar Ty0
env' Ty0
b
                          (Map TyVar Ty0, Ty0) -> TcM (Map TyVar Ty0, Ty0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map TyVar Ty0
env'', [Ty0] -> Ty0 -> Ty0
ArrowTy [Ty0]
as' Ty0
b')
       PackedTy String
t [Ty0]
tys -> do (Map TyVar Ty0
env', [Ty0]
tys') <- Map TyVar Ty0 -> [Ty0] -> TcM (Map TyVar Ty0, [Ty0])
gol Map TyVar Ty0
env [Ty0]
tys
                            (Map TyVar Ty0, Ty0) -> TcM (Map TyVar Ty0, Ty0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map TyVar Ty0
env', String -> [Ty0] -> Ty0
PackedTy String
t [Ty0]
tys')
       VectorTy Ty0
el_t -> do (Map TyVar Ty0
env', Ty0
el_t') <- Map TyVar Ty0 -> Ty0 -> TcM (Map TyVar Ty0, Ty0)
go Map TyVar Ty0
env Ty0
el_t
                           (Map TyVar Ty0, Ty0) -> TcM (Map TyVar Ty0, Ty0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map TyVar Ty0
env', Ty0 -> Ty0
VectorTy Ty0
el_t')
       ListTy Ty0
el_t -> do (Map TyVar Ty0
env', Ty0
el_t') <- Map TyVar Ty0 -> Ty0 -> TcM (Map TyVar Ty0, Ty0)
go Map TyVar Ty0
env Ty0
el_t
                         (Map TyVar Ty0, Ty0) -> TcM (Map TyVar Ty0, Ty0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map TyVar Ty0
env', Ty0 -> Ty0
ListTy Ty0
el_t')
       Ty0
ArenaTy  -> (Map TyVar Ty0, Ty0) -> TcM (Map TyVar Ty0, Ty0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map TyVar Ty0
env, Ty0
ty)
       Ty0
SymSetTy -> (Map TyVar Ty0, Ty0) -> TcM (Map TyVar Ty0, Ty0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map TyVar Ty0
env, Ty0
ty)
       Ty0
SymHashTy-> (Map TyVar Ty0, Ty0) -> TcM (Map TyVar Ty0, Ty0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map TyVar Ty0
env, Ty0
ty)
       Ty0
IntHashTy-> (Map TyVar Ty0, Ty0) -> TcM (Map TyVar Ty0, Ty0)
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map TyVar Ty0
env, Ty0
ty)

    gol :: M.Map TyVar Ty0 -> [Ty0] -> TcM (M.Map TyVar Ty0, [Ty0])
    gol :: Map TyVar Ty0 -> [Ty0] -> TcM (Map TyVar Ty0, [Ty0])
gol Map TyVar Ty0
env [Ty0]
tys = ((Map TyVar Ty0, [Ty0]) -> Ty0 -> TcM (Map TyVar Ty0, [Ty0]))
-> (Map TyVar Ty0, [Ty0]) -> [Ty0] -> TcM (Map TyVar Ty0, [Ty0])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM
                     (\(Map TyVar Ty0
env', [Ty0]
acc) Ty0
ty -> do
                         (Map TyVar Ty0
env'', Ty0
ty') <- Map TyVar Ty0 -> Ty0 -> TcM (Map TyVar Ty0, Ty0)
go Map TyVar Ty0
env' Ty0
ty
                         (Map TyVar Ty0, [Ty0]) -> TcM (Map TyVar Ty0, [Ty0])
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map TyVar Ty0
env'', [Ty0]
acc [Ty0] -> [Ty0] -> [Ty0]
forall a. [a] -> [a] -> [a]
++ [Ty0
ty']))
                     (Map TyVar Ty0
env, [])
                     [Ty0]
tys

--------------------------------------------------------------------------------
-- Unification
--------------------------------------------------------------------------------

unify :: Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify :: Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify Exp0
ex Ty0
ty1 Ty0
ty2
  | Ty0
ty1 Ty0 -> Ty0 -> Bool
forall a. Eq a => a -> a -> Bool
== Ty0
ty2 = --dbgTraceIt (sdoc ty1 ++ "/" ++ sdoc ty2) $
                 Subst -> TcM Subst
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst
emptySubst
  | Bool
otherwise  = -- dbgTraceIt (sdoc ty1 ++ "/" ++ sdoc ty2) $
      case (Ty0
ty1,Ty0
ty2) of
        (Ty0
IntTy, Ty0
IntTy)     -> Subst -> TcM Subst
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst
emptySubst
        (Ty0
FloatTy,Ty0
FloatTy)  -> Subst -> TcM Subst
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst
emptySubst
        (Ty0
BoolTy, Ty0
BoolTy)   -> Subst -> TcM Subst
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst
emptySubst
        (TyVar TyVar
_, TyVar TyVar
_) -> TcM Subst
fail_
        -- -- CHECKME
        -- (MetaTv a, MetaTv b) -> unifyVar ex a (MetaTv b)
        (MetaTv MetaTv
a, Ty0
_) -> Exp0 -> MetaTv -> Ty0 -> TcM Subst
unifyVar Exp0
ex MetaTv
a Ty0
ty2
        (Ty0
_, MetaTv MetaTv
b) -> Exp0 -> MetaTv -> Ty0 -> TcM Subst
unifyVar Exp0
ex MetaTv
b Ty0
ty1
        (ProdTy [Ty0]
as, ProdTy [Ty0]
bs) -> Exp0 -> [Ty0] -> [Ty0] -> TcM Subst
unifyl Exp0
ex [Ty0]
as [Ty0]
bs
        (ArrowTy [Ty0]
as Ty0
b, ArrowTy [Ty0]
cs Ty0
d) -> do
          Subst
s1 <- Exp0 -> [Ty0] -> [Ty0] -> TcM Subst
unifyl Exp0
ex [Ty0]
as [Ty0]
cs
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify Exp0
ex (Subst -> Ty0 -> Ty0
zonkTy Subst
s1 Ty0
b) (Subst -> Ty0 -> Ty0
zonkTy Subst
s1 Ty0
d)
          Subst -> TcM Subst
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s1)
        (PackedTy String
tc1 [Ty0]
tys1, PackedTy String
tc2 [Ty0]
tys2) ->
          if String
tc1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
tc2
          then Exp0 -> [Ty0] -> [Ty0] -> TcM Subst
unifyl Exp0
ex [Ty0]
tys1 [Ty0]
tys2
          else TcM Subst
fail_
        (SymDictTy Maybe Var
_ Ty0
t1, SymDictTy Maybe Var
_ Ty0
t2) -> Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify Exp0
ex Ty0
t1 Ty0
t2
        (VectorTy Ty0
t1, VectorTy Ty0
t2) -> Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify Exp0
ex Ty0
t1 Ty0
t2
        (ListTy Ty0
t1, ListTy Ty0
t2) -> Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify Exp0
ex Ty0
t1 Ty0
t2
        (PDictTy Ty0
k1 Ty0
v1, PDictTy Ty0
k2 Ty0
v2) -> do
          Subst
s1 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify Exp0
ex Ty0
k1 Ty0
k2
          Subst
s2 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify Exp0
ex Ty0
v1 Ty0
v2
          Subst -> TcM Subst
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2)
        (Ty0, Ty0)
_ -> Int -> String -> TcM Subst -> TcM Subst
forall a. Int -> String -> a -> a
dbgTrace Int
1 (String
"unify: Catch-all _; failed to unify " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Ty0 -> String
forall a. Out a => a -> String
sdoc Ty0
ty1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" with " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Ty0 -> String
forall a. Out a => a -> String
sdoc Ty0
ty2) TcM Subst
fail_
  where fail_ :: TcM Subst
fail_ = Doc -> TcM Subst
forall a. Doc -> TcM a
err (Doc -> TcM Subst) -> Doc -> TcM Subst
forall a b. (a -> b) -> a -> b
$  String -> Doc
text String
"Couldn't match type" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (Ty0 -> Doc
forall a. Out a => a -> Doc
doc Ty0
ty2)
                    Doc -> Doc -> Doc
<+> String -> Doc
text String
"with" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (Ty0 -> Doc
forall a. Out a => a -> Doc
doc Ty0
ty1)
                    Doc -> Doc -> Doc
$$ String -> Doc
text String
"Expected type:" Doc -> Doc -> Doc
<+> Ty0 -> Doc
forall a. Out a => a -> Doc
doc Ty0
ty1
                    Doc -> Doc -> Doc
$$ String -> Doc
text String
"Actual type:" Doc -> Doc -> Doc
<+> Ty0 -> Doc
forall a. Out a => a -> Doc
doc Ty0
ty2
                    Doc -> Doc -> Doc
$$ String -> Doc
text String
"In the expression: "
                    Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 (Exp0 -> Doc
forall a. Out a => a -> Doc
doc Exp0
ex)


unifyl :: Exp0 -> [Ty0] -> [Ty0] -> TcM Subst
unifyl :: Exp0 -> [Ty0] -> [Ty0] -> TcM Subst
unifyl Exp0
_ [] [] = Subst -> TcM Subst
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst
emptySubst
unifyl Exp0
e (Ty0
a:[Ty0]
as) (Ty0
b:[Ty0]
bs) = do
    -- N.B. We must apply s1 over the rest of the list before unifying it, i.e.
    --
    --     (<>) <$> unify e a b <*> unifyl e as bs
    --
    -- doesn't work!
    Subst
s1 <- Exp0 -> Ty0 -> Ty0 -> TcM Subst
unify Exp0
e Ty0
a Ty0
b
    Subst
s2 <- Exp0 -> [Ty0] -> [Ty0] -> TcM Subst
unifyl Exp0
e ((Ty0 -> Ty0) -> [Ty0] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Ty0 -> Ty0
zonkTy Subst
s1) [Ty0]
as) ((Ty0 -> Ty0) -> [Ty0] -> [Ty0]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Ty0 -> Ty0
zonkTy Subst
s1) [Ty0]
bs)
    Subst -> TcM Subst
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
s1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
s2)
unifyl Exp0
e [Ty0]
as [Ty0]
bs = Doc -> TcM Subst
forall a. Doc -> TcM a
err (Doc -> TcM Subst) -> Doc -> TcM Subst
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Couldn't unify:" Doc -> Doc -> Doc
<+> [Ty0] -> Doc
forall a. Out a => a -> Doc
doc [Ty0]
as Doc -> Doc -> Doc
<+> String -> Doc
text String
"and" Doc -> Doc -> Doc
<+> [Ty0] -> Doc
forall a. Out a => a -> Doc
doc [Ty0]
bs
                         Doc -> Doc -> Doc
$$ String -> Doc
text String
"In the expression: "
                         Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 (Exp0 -> Doc
forall a. Out a => a -> Doc
doc Exp0
e)

unifyVar :: Exp0 -> MetaTv -> Ty0 -> TcM Subst
unifyVar :: Exp0 -> MetaTv -> Ty0 -> TcM Subst
unifyVar Exp0
ex MetaTv
a Ty0
t
  | MetaTv -> Ty0 -> Bool
occursCheck MetaTv
a Ty0
t = Doc -> TcM Subst
forall a. Doc -> TcM a
err (Doc -> TcM Subst) -> Doc -> TcM Subst
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Occurs check: cannot construct the inifinite type: "
                              Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 (MetaTv -> Doc
forall a. Out a => a -> Doc
doc MetaTv
a Doc -> Doc -> Doc
<+> String -> Doc
text String
" ~ " Doc -> Doc -> Doc
<+> Ty0 -> Doc
forall a. Out a => a -> Doc
doc Ty0
t)
                              Doc -> Doc -> Doc
$$ String -> Doc
text String
"In the expression: "
                              Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 (Exp0 -> Doc
forall a. Out a => a -> Doc
doc Exp0
ex)
  | Bool
otherwise       = Subst -> TcM Subst
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst -> TcM Subst) -> Subst -> TcM Subst
forall a b. (a -> b) -> a -> b
$ Map MetaTv Ty0 -> Subst
Subst (MetaTv -> Ty0 -> Map MetaTv Ty0
forall k a. k -> a -> Map k a
M.singleton MetaTv
a Ty0
t)


occursCheck :: MetaTv -> Ty0 -> Bool
occursCheck :: MetaTv -> Ty0 -> Bool
occursCheck MetaTv
a Ty0
t = MetaTv
a MetaTv -> [MetaTv] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Ty0 -> [MetaTv]
metaTvsInTy Ty0
t

--------------------------------------------------------------------------------
-- Other helpers
--------------------------------------------------------------------------------

ensureEqualTy :: Exp0 -> Ty0 -> Ty0 -> TcM ()
ensureEqualTy :: Exp0 -> Ty0 -> Ty0 -> TcM ()
ensureEqualTy Exp0
ex Ty0
ty1 Ty0
ty2
  | Ty0
ty1 Ty0 -> Ty0 -> Bool
forall a. Eq a => a -> a -> Bool
== Ty0
ty2 = () -> TcM ()
forall a. a -> TcM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  | Bool
otherwise  = Doc -> TcM ()
forall a. Doc -> TcM a
err (Doc -> TcM ()) -> Doc -> TcM ()
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Couldn't match expected type:" Doc -> Doc -> Doc
<+> Ty0 -> Doc
forall a. Out a => a -> Doc
doc Ty0
ty1
                         Doc -> Doc -> Doc
$$ String -> Doc
text String
"with actual type: " Doc -> Doc -> Doc
<+> Ty0 -> Doc
forall a. Out a => a -> Doc
doc Ty0
ty2
                         Doc -> Doc -> Doc
$$ String -> Doc
text String
"In the expression: "
                         Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 (Exp0 -> Doc
forall a. Out a => a -> Doc
doc Exp0
ex)