simplify tuples

lib/Haskell/Law/Applicative/Def.agda

@@ -39,7 +39,3 @@ instance postulate
   iLawfulApplicativeTuple₂ : ⦃ Monoid a ⦄ → Applicative (a ×_)
 
   iLawfulApplicativeTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Applicative (a × b ×_)
-
-  iLawfulApplicativeTuple₄ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ →
-    Applicative (λ d → Tuple (a ∷ b ∷ c ∷ d ∷ []))
-

lib/Haskell/Law/Eq/Def.agda

@@ -85,9 +85,13 @@ postulate instance
 
   iLawfulEqUnit : IsLawfulEq ⊤
 
-  iLawfulEqTuple₀ : IsLawfulEq (Tuple [])
+  iLawfulEqTuple₂ : ⦃ iEqA : Eq a ⦄ ⦃ iEqB : Eq b ⦄
+                  → ⦃ IsLawfulEq a ⦄ → ⦃ IsLawfulEq b ⦄
+                  → IsLawfulEq (a × b)
 
-  iLawfulEqTuple : ⦃ iEqA : Eq a ⦄ → ⦃ iEqAs : Eq (Tuple as) ⦄ → ⦃ IsLawfulEq a ⦄ → ⦃ IsLawfulEq (Tuple as) ⦄ → IsLawfulEq (Tuple (a ∷ as))
+  iLawfulEqTuple₃ : ⦃ iEqA : Eq a ⦄ ⦃ iEqB : Eq b ⦄ ⦃ iEqC : Eq c ⦄
+                  → ⦃ IsLawfulEq a ⦄ → ⦃ IsLawfulEq b ⦄ → ⦃ IsLawfulEq c ⦄
+                  → IsLawfulEq (a × b × c)
 
   iLawfulEqList : ⦃ iEqA : Eq a ⦄ → ⦃ IsLawfulEq a ⦄ → IsLawfulEq (List a)
 

lib/Haskell/Law/Functor/Def.agda

@@ -22,6 +22,3 @@ instance postulate
   iLawfulFunctorTuple₂ : IsLawfulFunctor (a ×_)
 
   iLawfulFunctorTuple₃ : IsLawfulFunctor (a × b ×_)
-
-  iLawfulFunctorTuple₄ : IsLawfulFunctor (λ d → Tuple (a ∷ b ∷ c ∷ d ∷ []))
-

lib/Haskell/Law/Monad/Def.agda

@@ -44,7 +44,3 @@ instance postulate
   iLawfulMonadTuple₂ : ⦃ Monoid a ⦄ → Monad (a ×_)
 
   iLawfulMonadTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Monad (a × b ×_)
-
-  iLawfulMonadTuple₄ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ →
-    Monad (λ d → Tuple (a ∷ b ∷ c ∷ d ∷ []))
-

lib/Haskell/Law/Monoid/Def.agda

@@ -28,9 +28,11 @@ postulate instance
 
   iLawfulMonoidUnit : IsLawfulMonoid ⊤
 
-  iLawfulMonoidTuple₀ : IsLawfulMonoid (Tuple [])
+  iLawfulMonoidTuple₂ : ⦃ iSemA : Monoid a ⦄ ⦃ iSemB : Monoid b ⦄
+                      → ⦃ IsLawfulMonoid a ⦄ → ⦃ IsLawfulMonoid b ⦄
+                      → IsLawfulMonoid (a × b)
 
-  iLawfulMonoidTuple : ⦃ iSemA : Monoid a ⦄ → ⦃ iSemA : Monoid (Tuple as) ⦄
-    → ⦃ IsLawfulMonoid a ⦄ → ⦃ IsLawfulMonoid (Tuple as) ⦄
-    → IsLawfulMonoid (Tuple (a ∷ as))
+  iLawfulMonoidTuple₃ : ⦃ iSemA : Monoid a ⦄ ⦃ iSemB : Monoid b ⦄ ⦃ iSemC : Monoid c ⦄
+                      → ⦃ IsLawfulMonoid a ⦄ → ⦃ IsLawfulMonoid b ⦄ → ⦃ IsLawfulMonoid c ⦄
+                      → IsLawfulMonoid (a × b × c)
 

lib/Haskell/Law/Ord/Def.agda

@@ -162,9 +162,15 @@ postulate instance
 
   iLawfulOrdChar : IsLawfulOrd Char
 
-  iLawfulOrdTuple₀ : IsLawfulOrd (Tuple [])
+  iLawfulOrdUnit : IsLawfulOrd ⊤
 
-  iLawfulOrdTuple : ⦃ iOrdA : Ord a ⦄ → ⦃ iLawfulOrdA : Ord (Tuple as) ⦄ → ⦃ IsLawfulOrd a ⦄ → ⦃ IsLawfulOrd (Tuple as) ⦄ → IsLawfulOrd (Tuple (a ∷ as))
+  iLawfulOrdTuple₂ : ⦃ iOrdA : Ord a ⦄ ⦃ iOrdB : Ord b ⦄
+                   → ⦃ IsLawfulOrd a ⦄ → ⦃ IsLawfulOrd b ⦄
+                   → IsLawfulOrd (a × b)
+
+  iLawfulOrdTuple₃ : ⦃ iOrdA : Ord a ⦄ ⦃ iOrdB : Ord b ⦄ ⦃ iOrdC : Ord c ⦄
+                   → ⦃ IsLawfulOrd a ⦄ → ⦃ IsLawfulOrd b ⦄ → ⦃ IsLawfulOrd c ⦄
+                   → IsLawfulOrd (a × b × c)
 
   iLawfulOrdList : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄ → IsLawfulOrd (List a)
 

lib/Haskell/Law/Semigroup/Def.agda

@@ -17,9 +17,11 @@ postulate instance
 
   iLawfulSemigroupUnit : IsLawfulSemigroup ⊤
 
-  iLawfulSemigroupTuple₀ : IsLawfulSemigroup (Tuple [])
+  iLawfulSemigroupTuple₂ : ⦃ iSemA : Semigroup a ⦄ ⦃ iSemB : Semigroup b ⦄
+                         → ⦃ IsLawfulSemigroup a ⦄ → ⦃ IsLawfulSemigroup b ⦄
+                         → IsLawfulSemigroup (a × b)
 
-  iLawfulSemigroupTuple : ⦃ iSemA : Semigroup a ⦄ → ⦃ iSemA : Semigroup (Tuple as) ⦄
-    → ⦃ IsLawfulSemigroup a ⦄ → ⦃ IsLawfulSemigroup (Tuple as) ⦄
-    → IsLawfulSemigroup (Tuple (a ∷ as))
+  iLawfulSemigroupTuple₃ : ⦃ iSemA : Semigroup a ⦄ ⦃ iSemB : Semigroup b ⦄ ⦃ iSemC : Semigroup c ⦄
+                         → ⦃ IsLawfulSemigroup a ⦄ → ⦃ IsLawfulSemigroup b ⦄ → ⦃ IsLawfulSemigroup c ⦄
+                         → IsLawfulSemigroup (a × b × c)
 

lib/Haskell/Prim/Applicative.agda

@@ -77,14 +77,7 @@ instance
 
   iApplicativeTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Applicative (a × b ×_)
   iApplicativeTuple₃ = mkApplicative λ where
-    .pure x                          → mempty , mempty , x
-    ._<*>_ (a , b , f) (a₁ , b₁ , x) → a <> a₁ , b <> b₁ , f x
-
-  iApplicativeTuple₄ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ →
-    Applicative (λ d → Tuple (a ∷ b ∷ c ∷ d ∷ []))
-  iApplicativeTuple₄ = mkApplicative λ where
-    .pure x → mempty ; mempty ; mempty ; x ; tt
-    ._<*>_ (a ; b ; c ; f ; tt) (a₁ ; b₁ ; c₁ ; x ; tt) →
-      a <> a₁ ; b <> b₁ ; c <> c₁ ; f x ; tt
+    .pure x                → mempty , mempty , x
+    ._<*>_ (a , u , f) (b , v , x) → a <> b , u <> v , f x
 
 instance postulate iApplicativeIO : Applicative IO

lib/Haskell/Prim/Bounded.agda

@@ -59,15 +59,25 @@ instance
   iBoundedAboveChar : BoundedAbove Char
   iBoundedAboveChar .maxBound = '\1114111'
 
-  iBoundedBelowTuple₀ : BoundedBelow (Tuple [])
-  iBoundedBelowTuple₀ .minBound = tt
-  iBoundedAboveTuple₀ : BoundedAbove (Tuple [])
-  iBoundedAboveTuple₀ .maxBound = tt
-
-  iBoundedBelowTuple : ⦃ BoundedBelow a ⦄ → ⦃ BoundedBelow (Tuple as) ⦄ → BoundedBelow (Tuple (a ∷ as))
-  iBoundedBelowTuple .minBound = minBound ; minBound
-  iBoundedAboveTuple : ⦃ BoundedAbove a ⦄ → ⦃ BoundedAbove (Tuple as) ⦄ → BoundedAbove (Tuple (a ∷ as))
-  iBoundedAboveTuple .maxBound = maxBound ; maxBound
+  iBoundedBelowUnit : BoundedBelow ⊤
+  iBoundedBelowUnit .minBound = tt
+
+  iBoundedAboveUnit : BoundedAbove ⊤
+  iBoundedAboveUnit .maxBound = tt
+
+  iBoundedBelowTuple₂ : ⦃ BoundedBelow a ⦄ → ⦃ BoundedBelow b ⦄
+                      → BoundedBelow (a × b)
+  iBoundedBelowTuple₂ .minBound = minBound , minBound
+  iBoundedAboveTuple₂ : ⦃ BoundedAbove a ⦄ → ⦃ BoundedAbove b ⦄
+                      → BoundedAbove (a × b)
+  iBoundedAboveTuple₂ .maxBound = maxBound , maxBound
+
+  iBoundedBelowTuple₃ : ⦃ BoundedBelow a ⦄ → ⦃ BoundedBelow b ⦄ → ⦃ BoundedBelow c ⦄
+                      → BoundedBelow (a × b × c)
+  iBoundedBelowTuple₃ .minBound = minBound , minBound , minBound
+  iBoundedAboveTuple₃ : ⦃ BoundedAbove a ⦄ → ⦃ BoundedAbove b ⦄ → ⦃ BoundedAbove c ⦄
+                      → BoundedAbove (a × b × c)
+  iBoundedAboveTuple₃ .maxBound = maxBound , maxBound , maxBound
 
   iBoundedBelowOrdering : BoundedBelow Ordering
   iBoundedBelowOrdering .minBound = LT

lib/Haskell/Prim/Eq.agda

@@ -53,11 +53,11 @@ instance
   iEqUnit : Eq ⊤
   iEqUnit ._==_ _ _ = True
 
-  iEqTuple₀ : Eq (Tuple [])
-  iEqTuple₀ ._==_ _ _ = True
+  iEqTuple₂ : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → Eq (a × b)
+  iEqTuple₂ ._==_ (x₁ , y₁) (x₂ , y₂) = x₁ == x₂ && y₂ == y₂
 
-  iEqTuple : ⦃ Eq a ⦄ → ⦃ Eq (Tuple as) ⦄ → Eq (Tuple (a ∷ as))
-  iEqTuple ._==_ (x ; xs) (y ; ys) = x == y && xs == ys
+  iEqTuple₃ : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → ⦃ Eq c ⦄ → Eq (a × b × c)
+  iEqTuple₃ ._==_ (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) = x₁ == x₂ && y₂ == y₂ && z₁ == z₂
 
   iEqList : ⦃ Eq a ⦄ → Eq (List a)
   iEqList {a} ._==_ = eqList

lib/Haskell/Prim/Functor.agda

@@ -21,7 +21,7 @@ record Functor (f : Set → Set) : Set₁ where
     _<&>_ : f a → (a → b) → f b
     _<$_ : (@0 {{ b }} → a) → f b → f a
     _$>_ : f a → (@0 {{ a }} → b) → f b
-    void : f a → f (Tuple [])
+    void : f a → f ⊤
 -- ** defaults
 record DefaultFunctor (f : Set → Set) : Set₁ where
   field fmap : (a → b) → f a → f b
@@ -41,7 +41,7 @@ record DefaultFunctor (f : Set → Set) : Set₁ where
   _$>_ : f a → (@0 {{ a }} → b) → f b
   m $> x = x <$ m
 
-  void : f a → f (Tuple [])
+  void : f a → f ⊤
   void = tt <$_
 -- ** export
 open Functor ⦃...⦄ public
@@ -74,9 +74,6 @@ instance
   iFunctorTuple₂ = fmap= λ f (x , y) → x , f y
 
   iFunctorTuple₃ : Functor (a × b ×_)
-  iFunctorTuple₃ = fmap= λ f (x , y , z) → x , y , f z
-
-  iFunctorTuple₄ : Functor (λ d → Tuple (a ∷ b ∷ c ∷ d ∷ []))
-  iFunctorTuple₄ = fmap= λ f (x ; y ; z ; w ; tt) → x ; y ; z ; f w ; tt
+  iFunctorTuple₃ = fmap= λ where f (x , y , z) → x , y , f z
 
 instance postulate iFunctiorIO : Functor IO

lib/Haskell/Prim/Monad.agda

@@ -88,16 +88,10 @@ instance
   iMonadTuple₂ = bind= λ (a , x) k → first (a <>_) (k x)
 
   iMonadTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Monad (a × b ×_)
-  iMonadTuple₃ = bind= λ (a , b , x) k →
-    case k x of λ where
+  iMonadTuple₃ = bind= λ where
+    (a , b , x) k → case k x of λ where
       (a₁ , b₁ , y) → a <> a₁ , b <> b₁ , y
 
-  iMonadTuple₄ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ →
-                 Monad (λ d → Tuple (a ∷ b ∷ c ∷ d ∷ []))
-  iMonadTuple₄ = bind= λ (a ; b ; c ; x ; tt) k →
-    case k x of λ where
-      (a₁ ; b₁ ; c₁ ; y ; tt) → a <> a₁ ; b <> b₁ ; c <> c₁ ; y ; tt
-
 instance postulate iMonadIO : Monad IO
 
 record MonadFail (m : Set → Set) : Set₁ where

lib/Haskell/Prim/Monoid.agda

@@ -36,11 +36,12 @@ instance
   iSemigroupUnit : Semigroup ⊤
   iSemigroupUnit ._<>_ _ _ = tt
 
-  iSemigroupTuple₀ : Semigroup (Tuple [])
-  iSemigroupTuple₀ ._<>_ _ _ = tt
 
-  iSemigroupTuple : ⦃ Semigroup a ⦄ → ⦃ Semigroup (Tuple as) ⦄ → Semigroup (Tuple (a ∷ as))
-  iSemigroupTuple ._<>_ (x ; xs) (y ; ys) = x <> y ; xs <> ys
+  iSemigroupTuple₂ : ⦃ Semigroup a ⦄ → ⦃ Semigroup b ⦄ → Semigroup (a × b)
+  iSemigroupTuple₂ ._<>_ (x₁ , y₁) (x₂ , y₂) = x₁ <> x₂ , y₁ <> y₂
+
+  iSemigroupTuple₃ : ⦃ Semigroup a ⦄ → ⦃ Semigroup b ⦄ → ⦃ Semigroup c ⦄ → Semigroup (a × b × c)
+  iSemigroupTuple₃ ._<>_ (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) = x₁ <> x₂ , y₁ <> y₂ , z₁ <> z₂
 
 
 --------------------------------------------------
@@ -89,11 +90,11 @@ instance
   iMonoidUnit : Monoid ⊤
   iMonoidUnit = mempty= tt
 
-  iMonoidTuple₀ : Monoid (Tuple [])
-  iMonoidTuple₀ = mempty= tt
+  iMonoidTuple₂ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Monoid (a × b)
+  iMonoidTuple₂ = mempty= (mempty , mempty)
 
-  iMonoidTuple : ⦃ Monoid a ⦄ → ⦃ Monoid (Tuple as) ⦄ → Monoid (Tuple (a ∷ as))
-  iMonoidTuple = mempty= mempty ; mempty
+  iMonoidTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ →  Monoid (a × b × c)
+  iMonoidTuple₃ = mempty= (mempty , mempty , mempty)
 
 open DefaultMonoid
 

lib/Haskell/Prim/Ord.agda

@@ -125,11 +125,16 @@ instance
     True  False → GT
     _     _     → EQ
 
-  iOrdTuple₀ : Ord (Tuple [])
-  iOrdTuple₀ = ordFromCompare λ _ _ → EQ
+  iOrdUnit : Ord ⊤
+  iOrdUnit = ordFromCompare λ _ _ → EQ
 
-  iOrdTuple : ⦃ Ord a ⦄ → ⦃ Ord (Tuple as) ⦄ → Ord (Tuple (a ∷ as))
-  iOrdTuple = ordFromCompare λ where (x ; xs) (y ; ys) → compare x y <> compare xs ys
+  iOrdTuple₂ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → Ord (a × b)
+  iOrdTuple₂ = ordFromCompare λ where
+    (x₁ , y₁) (x₂ , y₂) → compare x₁ x₂ <> compare y₁ y₂
+
+  iOrdTuple₃ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → ⦃ Ord c ⦄ → Ord (a × b × c)
+  iOrdTuple₃ = ordFromCompare λ where
+    (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) → compare x₁ x₂ <> compare y₁ y₂ <> compare z₁ z₂
 
 compareList : ⦃ Ord a ⦄ → List a → List a → Ordering
 compareList []       []       = EQ

lib/Haskell/Prim/Show.agda

@@ -117,13 +117,12 @@ instance
   iShowEither = showsPrec= λ where
     p (Left  x) → showApp₁ p "Left"  x
     p (Right y) → showApp₁ p "Right" y
-private
-  -- Minus the parens
-  showTuple : ⦃ All Show as ⦄ → Tuple as → ShowS
-  showTuple ⦃ allNil  ⦄                 _        = showString ""
-  showTuple ⦃ allCons ⦃ is = allNil ⦄ ⦄ (x ; tt) = shows x
-  showTuple ⦃ allCons ⦄                 (x ; xs) = shows x
-                                                 ∘ showString ", " ∘ showTuple xs
+
 instance
-  iShowTuple : ⦃ All Show as ⦄ → Show (Tuple as)
-  iShowTuple = showsPrec= λ _ → showParen True ∘ showTuple
+  iShowTuple₂ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show (a × b)
+  iShowTuple₂ = showsPrec= λ _ → λ where
+    (x , y) → showString "(" ∘ shows x ∘ showString ", " ∘ shows y ∘ showString ")"
+
+  iShowTuple₃ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → ⦃ Show c ⦄ → Show (a × b × c)
+  iShowTuple₃ = showsPrec= λ _ → λ where
+    (x , y , z) → showString "(" ∘ shows x ∘ showString ", " ∘ shows y ∘ showString ", " ∘ shows z ∘ showString ")"

lib/Haskell/Prim/Tuple.agda

@@ -3,46 +3,29 @@ module Haskell.Prim.Tuple where
 
 open import Haskell.Prim
 
-variable
-  as : List Set
-
 --------------------------------------------------
 -- Tuples
 
-infixr 5 _;_
-record Pair (A B : Set) : Set where
-  constructor _;_
-  field fst : A ; snd : B
-
-Tuple : List Set → Set
-Tuple [] = ⊤
-Tuple (A ∷ AS) = Pair A (Tuple AS)
-
 infix 3 _×_ _×_×_
 
-_×_ : (a b : Set) → Set
-a × b = Tuple (a ∷ b ∷ [])
-
-_×_×_ : (a b c : Set) → Set
-a × b × c = Tuple (a ∷ b ∷ c ∷ [])
-
 infix -1 _,_ _,_,_
 
-pattern _,_     x y     = x ; y ; tt
-pattern _,_,_   x y z   = x ; y ; z ; tt
+record _×_ (a b : Set) : Set where
+  constructor _,_
+  field
+    fst : a
+    snd : b
+open _×_ public
+
+data _×_×_ (a b c : Set) : Set where
+  _,_,_ : a → b → c → a × b × c
 
 uncurry : (a → b → c) → a × b → c
 uncurry f (x , y) = f x y
 
 curry : (a × b → c) → a → b → c
 curry f x y = f (x , y)
 
-fst : a × b → a
-fst (x , _) = x
-
-snd : a × b → b
-snd (_ , y) = y
-
 first : (a → b) → a × c → b × c
 first f (x , y) = f x , y
 

src/Agda2Hs/Compile/Function.hs

@@ -44,7 +44,7 @@ import Agda.TypeChecking.Datatypes (isDataOrRecord)
 
 isSpecialPat :: QName -> Maybe (ConHead -> ConPatternInfo -> [NamedArg DeBruijnPattern] -> C (Hs.Pat ()))
 isSpecialPat qn = case prettyShow qn of
-  "Haskell.Prim.Tuple._;_" -> Just tuplePat
+  "Haskell.Prim.Tuple._,_"   -> Just tuplePat
   "Agda.Builtin.Int.Int.pos" -> Just posIntPat
   "Agda.Builtin.Int.Int.negsuc" -> Just negSucIntPat
   s | s `elem` badConstructors -> Just $ \ _ _ _ -> genericDocError =<<
@@ -61,14 +61,7 @@ isUnboxCopattern (ProjP _ q) = isJust <$> isUnboxProjection q
 isUnboxCopattern _           = return False
 
 tuplePat :: ConHead -> ConPatternInfo -> [NamedArg DeBruijnPattern] -> C (Hs.Pat ())
-tuplePat cons i ps = do
-  let p = ConP cons i ps
-      err = sep [ "Tuple pattern"
-                , nest 2 $ prettyTCM p
-                , "does not have a known size." ]
-  xs <- makeListP' "Agda.Builtin.Unit.tt" "Haskell.Prim.Tuple._;_" err p
-  qs <- mapM compilePat xs
-  return $ Hs.PTuple () Hs.Boxed qs
+tuplePat cons i ps = mapM (compilePat . namedArg) ps <&> Hs.PTuple () Hs.Boxed
 
 -- Agda2Hs does not support natural number patterns directly (since
 -- they don't exist in Haskell), however they occur as part of

src/Agda2Hs/Compile/Term.hs

@@ -53,18 +53,12 @@ isSpecialTerm q = case prettyShow q of
 
 isSpecialCon :: QName -> Maybe (ConHead -> ConInfo -> Elims -> C (Hs.Exp ()))
 isSpecialCon = prettyShow >>> \case
-  "Haskell.Prim.Tuple._;_" -> Just tupleTerm
+  "Haskell.Prim.Tuple._,_"         -> Just tupleTerm
+  "Haskell.Prim.Tuple._×_×_._,_,_" -> Just tupleTerm
   _ -> Nothing
 
 tupleTerm :: ConHead -> ConInfo -> Elims -> C (Hs.Exp ())
-tupleTerm cons i es = do
-  let v   = Con cons i es
-      err = sep [ text "Tuple value"
-                , nest 2 $ prettyTCM v
-                , text "does not have a known size." ]
-  xs <- makeList' "Agda.Builtin.Unit.tt" "Haskell.Prim.Tuple._;_" err v
-  ts <- mapM compileTerm xs
-  return $ Hs.Tuple () Hs.Boxed ts
+tupleTerm cons i es = compileElims es <&> Hs.Tuple () Hs.Boxed
 
 ifThenElse :: QName -> Elims -> C (Hs.Exp ())
 ifThenElse _ es = compileElims es >>= \case