module Language.Lambda.SystemF.Expression
  ( SystemFExpr(..),
    TypedExpr(..),
    Ty(..),
    _expr,
    _ty,
    prettyPrint,
    substituteTy,
    upperLambda
  ) where

import Data.Monoid
import Prettyprinter
import Prettyprinter.Render.Text (renderStrict)
import RIO

data SystemFExpr name
  -- | A global binding: `let x = y`
  = Let name (SystemFExpr name)
  -- | Variable: `x`
  | Var name
  -- | Variable annotated with type: `x:T`
  | VarAnn name (Ty name)
  -- | Function application: `x y`
  | App (SystemFExpr name) (SystemFExpr name)
  -- | Lambda abstraction: `\x: X. x`
  | Abs name (Ty name) (SystemFExpr name)
  -- | Type Abstraction: `\X. body`
  | TyAbs name (SystemFExpr name)
  -- | Type Application: `x [X]`
  | TyApp (SystemFExpr name) (Ty name)
  deriving (SystemFExpr name -> SystemFExpr name -> Bool
forall name.
Eq name =>
SystemFExpr name -> SystemFExpr name -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SystemFExpr name -> SystemFExpr name -> Bool
$c/= :: forall name.
Eq name =>
SystemFExpr name -> SystemFExpr name -> Bool
== :: SystemFExpr name -> SystemFExpr name -> Bool
$c== :: forall name.
Eq name =>
SystemFExpr name -> SystemFExpr name -> Bool
Eq, Int -> SystemFExpr name -> ShowS
forall name. Show name => Int -> SystemFExpr name -> ShowS
forall name. Show name => [SystemFExpr name] -> ShowS
forall name. Show name => SystemFExpr name -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SystemFExpr name] -> ShowS
$cshowList :: forall name. Show name => [SystemFExpr name] -> ShowS
show :: SystemFExpr name -> String
$cshow :: forall name. Show name => SystemFExpr name -> String
showsPrec :: Int -> SystemFExpr name -> ShowS
$cshowsPrec :: forall name. Show name => Int -> SystemFExpr name -> ShowS
Show)

data TypedExpr name = TypedExpr
  { forall name. TypedExpr name -> SystemFExpr name
teExpr :: SystemFExpr name,
    forall name. TypedExpr name -> Ty name
teTy :: Ty name
  } deriving (TypedExpr name -> TypedExpr name -> Bool
forall name. Eq name => TypedExpr name -> TypedExpr name -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypedExpr name -> TypedExpr name -> Bool
$c/= :: forall name. Eq name => TypedExpr name -> TypedExpr name -> Bool
== :: TypedExpr name -> TypedExpr name -> Bool
$c== :: forall name. Eq name => TypedExpr name -> TypedExpr name -> Bool
Eq, Int -> TypedExpr name -> ShowS
forall name. Show name => Int -> TypedExpr name -> ShowS
forall name. Show name => [TypedExpr name] -> ShowS
forall name. Show name => TypedExpr name -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypedExpr name] -> ShowS
$cshowList :: forall name. Show name => [TypedExpr name] -> ShowS
show :: TypedExpr name -> String
$cshow :: forall name. Show name => TypedExpr name -> String
showsPrec :: Int -> TypedExpr name -> ShowS
$cshowsPrec :: forall name. Show name => Int -> TypedExpr name -> ShowS
Show)

data Ty name
  = TyVar name                  -- ^ Type variable (T)
  | TyArrow (Ty name) (Ty name) -- ^ Type arrow    (T -> U)
  | TyForAll name (Ty name)     -- ^ Universal type (forall T. X)
  deriving (Int -> Ty name -> ShowS
forall name. Show name => Int -> Ty name -> ShowS
forall name. Show name => [Ty name] -> ShowS
forall name. Show name => Ty name -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Ty name] -> ShowS
$cshowList :: forall name. Show name => [Ty name] -> ShowS
show :: Ty name -> String
$cshow :: forall name. Show name => Ty name -> String
showsPrec :: Int -> Ty name -> ShowS
$cshowsPrec :: forall name. Show name => Int -> Ty name -> ShowS
Show)

instance (Pretty name) => Pretty (SystemFExpr name) where
  pretty :: forall ann. SystemFExpr name -> Doc ann
pretty (Var name
name) = forall a ann. Pretty a => a -> Doc ann
pretty name
name
  pretty (VarAnn name
name Ty name
ty) = forall name a. Pretty name => name -> Ty name -> Doc a
prettyVarAnn name
name Ty name
ty
  pretty (App SystemFExpr name
e1 SystemFExpr name
e2) = forall name a.
Pretty name =>
SystemFExpr name -> SystemFExpr name -> Doc a
prettyApp SystemFExpr name
e1 SystemFExpr name
e2
  pretty (Abs name
name Ty name
ty SystemFExpr name
body) = forall name ann.
Pretty name =>
name -> Ty name -> SystemFExpr name -> Doc ann
prettyAbs name
name Ty name
ty SystemFExpr name
body
  pretty (Let name
name SystemFExpr name
expr) = forall name ann. Pretty name => name -> SystemFExpr name -> Doc ann
prettyLet name
name SystemFExpr name
expr
  pretty (TyAbs name
ty SystemFExpr name
body) = forall name ann. Pretty name => name -> SystemFExpr name -> Doc ann
prettyTyAbs name
ty SystemFExpr name
body
  pretty (TyApp SystemFExpr name
expr Ty name
ty) = forall name ann.
Pretty name =>
SystemFExpr name -> Ty name -> Doc ann
prettyTyApp SystemFExpr name
expr Ty name
ty

instance Pretty name => Pretty (TypedExpr name) where
  pretty :: forall ann. TypedExpr name -> Doc ann
pretty TypedExpr name
expr = forall a ann. Pretty a => a -> Doc ann
pretty (TypedExpr name
expr forall s a. s -> Getting a s a -> a
^. forall name. Lens' (TypedExpr name) (SystemFExpr name)
_expr) forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann
colon forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (TypedExpr name
expr forall s a. s -> Getting a s a -> a
^. forall name. Lens' (TypedExpr name) (Ty name)
_ty)

instance Pretty name => Pretty (Ty name) where
  pretty :: forall ann. Ty name -> Doc ann
pretty = forall name ann. Pretty name => Bool -> Ty name -> Doc ann
prettyTy Bool
False

instance Eq name => Eq (Ty name) where
  == :: Ty name -> Ty name -> Bool
(==) = forall name. Eq name => Ty name -> Ty name -> Bool
isTyEquivalent

_expr :: Lens' (TypedExpr name) (SystemFExpr name)
_expr :: forall name. Lens' (TypedExpr name) (SystemFExpr name)
_expr = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens forall name. TypedExpr name -> SystemFExpr name
teExpr (\TypedExpr name
res SystemFExpr name
expr -> TypedExpr name
res { teExpr :: SystemFExpr name
teExpr = SystemFExpr name
expr })

_ty :: Lens' (TypedExpr name) (Ty name)
_ty :: forall name. Lens' (TypedExpr name) (Ty name)
_ty = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens forall name. TypedExpr name -> Ty name
teTy (\TypedExpr name
res Ty name
ty -> TypedExpr name
res { teTy :: Ty name
teTy = Ty name
ty })

prettyPrint :: Pretty pretty => pretty -> Text
prettyPrint :: forall pretty. Pretty pretty => pretty -> Text
prettyPrint pretty
expr = forall ann. SimpleDocStream ann -> Text
renderStrict SimpleDocStream Any
docStream
  where docStream :: SimpleDocStream Any
docStream = forall ann. LayoutOptions -> Doc ann -> SimpleDocStream ann
layoutPretty LayoutOptions
defaultLayoutOptions (forall a ann. Pretty a => a -> Doc ann
pretty pretty
expr)

substituteTy
  :: Eq name
  => Ty name
  -> name
  -> Ty name
  -> Ty name
substituteTy :: forall name. Eq name => Ty name -> name -> Ty name -> Ty name
substituteTy Ty name
ty name
forName Ty name
inTy
  = case Ty name
inTy of
      TyVar name
n
        | name
n forall a. Eq a => a -> a -> Bool
== name
forName -> Ty name
ty
        | Bool
otherwise -> Ty name
inTy
      TyArrow Ty name
t1 Ty name
t2 -> forall name. Ty name -> Ty name -> Ty name
TyArrow (Ty name -> Ty name
sub Ty name
t1) (Ty name -> Ty name
sub Ty name
t2)
      TyForAll name
n Ty name
ty'
        | name
n forall a. Eq a => a -> a -> Bool
== name
forName -> Ty name
inTy
        | Bool
otherwise -> forall name. name -> Ty name -> Ty name
TyForAll name
n (Ty name -> Ty name
sub Ty name
ty')
  where sub :: Ty name -> Ty name
sub = forall name. Eq name => Ty name -> name -> Ty name -> Ty name
substituteTy Ty name
ty name
forName

upperLambda :: Char
upperLambda :: Char
upperLambda = Char
'Λ'

prettyVarAnn :: Pretty name => name -> Ty name -> Doc a
prettyVarAnn :: forall name a. Pretty name => name -> Ty name -> Doc a
prettyVarAnn name
var Ty name
ty = forall a ann. Pretty a => a -> Doc ann
pretty name
var forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
colon forall a. Semigroup a => a -> a -> a
<> Ty name -> Doc a
prettyTy' Ty name
ty
  where prettyTy' :: Ty name -> Doc a
prettyTy' (TyVar name
_) = forall name ann. Pretty name => Bool -> Ty name -> Doc ann
prettyTy Bool
True Ty name
ty
        prettyTy' Ty name
_ = forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall name ann. Pretty name => Bool -> Ty name -> Doc ann
prettyTy Bool
True Ty name
ty

prettyApp
  :: Pretty name
  => SystemFExpr name
  -> SystemFExpr name
  -> Doc a
prettyApp :: forall name a.
Pretty name =>
SystemFExpr name -> SystemFExpr name -> Doc a
prettyApp e1 :: SystemFExpr name
e1@Abs{} e2 :: SystemFExpr name
e2@Abs{} = forall ann. Doc ann -> Doc ann
parens (forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
e1) forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
parens (forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
e2)
prettyApp e1 :: SystemFExpr name
e1@Abs{} SystemFExpr name
e2 = forall ann. Doc ann -> Doc ann
parens (forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
e1) forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
e2
prettyApp SystemFExpr name
e1 e2 :: SystemFExpr name
e2@Abs{} = forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
e1 forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
parens (forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
e2)
prettyApp SystemFExpr name
e1 e2 :: SystemFExpr name
e2@App{} = forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
e1 forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
parens (forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
e2)
prettyApp SystemFExpr name
e1 SystemFExpr name
e2 = forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
e1 forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
e2

prettyAbs
  :: Pretty name
  => name
  -> Ty name
  -> SystemFExpr name
  -> Doc ann
prettyAbs :: forall name ann.
Pretty name =>
name -> Ty name -> SystemFExpr name -> Doc ann
prettyAbs name
name Ty name
ty SystemFExpr name
body
  = forall ann. Doc ann
lambda
    forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. [Doc ann] -> Doc ann
hsep (forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall name ty ann.
(Pretty name, Pretty ty) =>
name -> Ty ty -> Doc ann
prettyArg) [(name, Ty name)]
names)
    forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
dot
    forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
body'
  where ([(name, Ty name)]
names, SystemFExpr name
body') = forall n.
n -> Ty n -> SystemFExpr n -> ([(n, Ty n)], SystemFExpr n)
uncurryAbs name
name Ty name
ty SystemFExpr name
body

prettyLet :: Pretty name => name -> SystemFExpr name -> Doc ann
prettyLet :: forall name ann. Pretty name => name -> SystemFExpr name -> Doc ann
prettyLet name
name SystemFExpr name
expr = Doc ann
"let" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty name
name forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann
equals forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
expr

prettyTyAbs :: (Pretty name) => name -> SystemFExpr name -> Doc ann
prettyTyAbs :: forall name ann. Pretty name => name -> SystemFExpr name -> Doc ann
prettyTyAbs name
name SystemFExpr name
body = forall ann. Doc ann
upperLambda' forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. [Doc ann] -> Doc ann
hsep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [name]
names) forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
dot
    forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
body'
  where ([name]
names, SystemFExpr name
body') = forall n. n -> SystemFExpr n -> ([n], SystemFExpr n)
uncurryTyAbs name
name SystemFExpr name
body
prettyTyApp :: (Pretty name) => SystemFExpr name -> Ty name -> Doc ann
prettyTyApp :: forall name ann.
Pretty name =>
SystemFExpr name -> Ty name -> Doc ann
prettyTyApp SystemFExpr name
expr Ty name
ty = forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
expr forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
brackets (forall a ann. Pretty a => a -> Doc ann
pretty Ty name
ty)

prettyTy :: Pretty name => Bool -> Ty name -> Doc ann
prettyTy :: forall name ann. Pretty name => Bool -> Ty name -> Doc ann
prettyTy Bool
_ (TyVar name
name) = forall a ann. Pretty a => a -> Doc ann
pretty name
name
prettyTy Bool
compact (TyArrow Ty name
t1 Ty name
t2) = forall name ann.
Pretty name =>
Bool -> Ty name -> Ty name -> Doc ann
prettyTyArrow Bool
compact Ty name
t1 Ty name
t2
prettyTy Bool
compact (TyForAll name
name Ty name
ty) = forall name ann. Pretty name => Bool -> name -> Ty name -> Doc ann
prettyTyForAll Bool
compact name
name Ty name
ty

isTyEquivalent :: Eq name => Ty name -> Ty name -> Bool
isTyEquivalent :: forall name. Eq name => Ty name -> Ty name -> Bool
isTyEquivalent Ty name
t1 Ty name
t2
  | Ty name
t1 forall name. Eq name => Ty name -> Ty name -> Bool
`isTySame` Ty name
t2 = Bool
True
  | Bool
otherwise = case (Ty name
t1, Ty name
t2) of
      (TyForAll name
n1 Ty name
t1', TyForAll name
n2 Ty name
t2') -> (name
n1, Ty name
t1') forall name. Eq name => (name, Ty name) -> (name, Ty name) -> Bool
`areForAllsEquivalent` (name
n2, Ty name
t2')
      (Ty name, Ty name)
_ -> Bool
False

prettyTyArrow :: Pretty name => Bool -> Ty name -> Ty name -> Doc ann
prettyTyArrow :: forall name ann.
Pretty name =>
Bool -> Ty name -> Ty name -> Doc ann
prettyTyArrow Bool
compact (TyArrow Ty name
t1 Ty name
t2) Ty name
t3
  = forall ann. Bool -> Doc ann -> Doc ann -> Doc ann
prettyTyArrow' Bool
compact Doc ann
compositeTy forall a b. (a -> b) -> a -> b
$ forall name ann. Pretty name => Bool -> Ty name -> Doc ann
prettyTy Bool
compact Ty name
t3
  where compositeTy :: Doc ann
compositeTy = forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall name ann.
Pretty name =>
Bool -> Ty name -> Ty name -> Doc ann
prettyTyArrow Bool
compact Ty name
t1 Ty name
t2

prettyTyArrow Bool
compact Ty name
t1 Ty name
t2
  = forall ann. Bool -> Doc ann -> Doc ann -> Doc ann
prettyTyArrow' Bool
compact (forall name ann. Pretty name => Bool -> Ty name -> Doc ann
prettyTy Bool
compact Ty name
t1) (forall name ann. Pretty name => Bool -> Ty name -> Doc ann
prettyTy Bool
compact Ty name
t2)

prettyTyForAll :: Pretty name => Bool -> name -> Ty name -> Doc ann
prettyTyForAll :: forall name ann. Pretty name => Bool -> name -> Ty name -> Doc ann
prettyTyForAll Bool
compact name
name Ty name
ty
  = Doc ann
"forall"
  forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty name
name forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
dot
  forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall name ann. Pretty name => Bool -> Ty name -> Doc ann
prettyTy Bool
compact Ty name
ty

lambda :: Doc ann
lambda :: forall ann. Doc ann
lambda = forall a ann. Pretty a => a -> Doc ann
pretty Char
'λ'

prettyArg :: (Pretty name, Pretty ty) => name -> Ty ty -> Doc ann
prettyArg :: forall name ty ann.
(Pretty name, Pretty ty) =>
name -> Ty ty -> Doc ann
prettyArg name
name (TyArrow Ty ty
t1 Ty ty
t2)
  = forall a ann. Pretty a => a -> Doc ann
pretty name
name forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
colon forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
parens (forall name ann.
Pretty name =>
Bool -> Ty name -> Ty name -> Doc ann
prettyTyArrow Bool
True Ty ty
t1 Ty ty
t2)
prettyArg name
name Ty ty
ty = forall a ann. Pretty a => a -> Doc ann
pretty name
name forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
colon forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty Ty ty
ty

upperLambda' :: Doc ann
upperLambda' :: forall ann. Doc ann
upperLambda' = forall a ann. Pretty a => a -> Doc ann
pretty Char
upperLambda

isTySame :: Eq name => Ty name -> Ty name -> Bool
isTySame :: forall name. Eq name => Ty name -> Ty name -> Bool
isTySame (TyVar name
n1) (TyVar name
n2) = name
n1 forall a. Eq a => a -> a -> Bool
== name
n2
isTySame (TyArrow Ty name
t1 Ty name
t2) (TyArrow Ty name
t1' Ty name
t2') = Ty name
t1 forall a. Eq a => a -> a -> Bool
== Ty name
t1' Bool -> Bool -> Bool
&& Ty name
t2 forall a. Eq a => a -> a -> Bool
== Ty name
t2'
isTySame (TyForAll name
n1 Ty name
t1) (TyForAll name
n2 Ty name
t2) = name
n1 forall a. Eq a => a -> a -> Bool
== name
n2 Bool -> Bool -> Bool
&& Ty name
t1 forall a. Eq a => a -> a -> Bool
== Ty name
t2
isTySame Ty name
_ Ty name
_ = Bool
False

areForAllsEquivalent :: Eq name => (name, Ty name) -> (name, Ty name) -> Bool
areForAllsEquivalent :: forall name. Eq name => (name, Ty name) -> (name, Ty name) -> Bool
areForAllsEquivalent (name
n1, Ty name
t1) (name
n2, Ty name
t2) = Ty name
t1 forall a. Eq a => a -> a -> Bool
== forall name. Eq name => Ty name -> name -> Ty name -> Ty name
substituteTy (forall name. name -> Ty name
TyVar name
n1) name
n2 Ty name
t2

prettyTyArrow' :: Bool -> Doc ann -> Doc ann -> Doc ann
prettyTyArrow' :: forall ann. Bool -> Doc ann -> Doc ann -> Doc ann
prettyTyArrow' Bool
compact Doc ann
doc1 Doc ann
doc2 = Doc ann
doc1 Doc ann -> Doc ann -> Doc ann
`add'` Doc ann
"->" Doc ann -> Doc ann -> Doc ann
`add'` Doc ann
doc2
  where add' :: Doc ann -> Doc ann -> Doc ann
add'
          | Bool
compact = forall a. Semigroup a => a -> a -> a
(<>) 
          | Bool
otherwise = forall ann. Doc ann -> Doc ann -> Doc ann
(<+>)

uncurryAbs :: n -> Ty n -> SystemFExpr n -> ([(n, Ty n)], SystemFExpr n)
uncurryAbs :: forall n.
n -> Ty n -> SystemFExpr n -> ([(n, Ty n)], SystemFExpr n)
uncurryAbs n
name Ty n
ty = forall {a}.
[(a, Ty a)] -> SystemFExpr a -> ([(a, Ty a)], SystemFExpr a)
uncurry' [(n
name, Ty n
ty)] 
  where uncurry' :: [(a, Ty a)] -> SystemFExpr a -> ([(a, Ty a)], SystemFExpr a)
uncurry' [(a, Ty a)]
ns (Abs a
n' Ty a
t' SystemFExpr a
body') = [(a, Ty a)] -> SystemFExpr a -> ([(a, Ty a)], SystemFExpr a)
uncurry' ((a
n', Ty a
t')forall a. a -> [a] -> [a]
:[(a, Ty a)]
ns) SystemFExpr a
body'
        uncurry' [(a, Ty a)]
ns SystemFExpr a
body'             = (forall a. [a] -> [a]
reverse [(a, Ty a)]
ns, SystemFExpr a
body')

uncurryTyAbs :: n -> SystemFExpr n -> ([n], SystemFExpr n)
uncurryTyAbs :: forall n. n -> SystemFExpr n -> ([n], SystemFExpr n)
uncurryTyAbs n
ty = forall {a}. [a] -> SystemFExpr a -> ([a], SystemFExpr a)
uncurry' [n
ty]
  where uncurry' :: [a] -> SystemFExpr a -> ([a], SystemFExpr a)
uncurry' [a]
ts (TyAbs a
t' SystemFExpr a
body') = [a] -> SystemFExpr a -> ([a], SystemFExpr a)
uncurry' (a
t'forall a. a -> [a] -> [a]
:[a]
ts) SystemFExpr a
body'
        uncurry' [a]
ts SystemFExpr a
body'            = (forall a. [a] -> [a]
reverse [a]
ts, SystemFExpr a
body')