Merge pull request #1386 from Russoul/prelude-interface-constructors

[prelude] Add explicit constructor to every interface

docs/source/tutorial/interfaces.rst

@@ -721,6 +721,25 @@ do this with a ``using`` clause in the implementation as follows:
 The ``using PlusNatSemi`` clause indicates that ``PlusNatMonoid`` should
 extend ``PlusNatSemi`` specifically.
 
+.. _InterfaceConstructors:
+
+Interface Constructors
+======================
+
+Interfaces, just like records, can be declared with a user-defined constructor.
+
+.. code-block:: idris
+
+    interface A a where
+      getA : a
+
+    interface A t => B t where
+      constructor MkB
+
+      getB : t
+
+Then ``MkB : A t => t -> B t``.
+
 .. _DeterminingParameters:
 
 Determining Parameters

libs/prelude/Builtin.idr

@@ -207,6 +207,7 @@ force x = Force x
 ||| Interface for types that can be constructed from string literals.
 public export
 interface FromString ty where
+  constructor MkFromString
   ||| Conversion from String.
   fromString : String -> ty
 

libs/prelude/Prelude/Cast.idr

@@ -14,6 +14,7 @@ import Prelude.Types
 ||| Interface for transforming an instance of a data type to another type.
 public export
 interface Cast from to where
+  constructor MkCast
   ||| Perform a (potentially lossy!) cast operation.
   ||| @ orig The original type
   cast : (orig : from) -> to

libs/prelude/Prelude/EqOrd.idr

@@ -13,6 +13,7 @@ import Prelude.Ops
 ||| The Eq interface defines inequality and equality.
 public export
 interface Eq ty where
+  constructor MkEq
   (==) : ty -> ty -> Bool
   (/=) : ty -> ty -> Bool
 
@@ -86,6 +87,7 @@ Eq Ordering where
 ||| The Ord interface defines comparison operations on ordered data types.
 public export
 interface Eq ty => Ord ty where
+  constructor MkOrd
   compare : ty -> ty -> Ordering
 
   (<) : ty -> ty -> Bool

libs/prelude/Prelude/IO.idr

@@ -32,10 +32,12 @@ Monad IO where
 
 public export
 interface Monad io => HasIO io where
+  constructor MkHasIO
   liftIO : IO a -> io a
 
 public export
 interface Monad io => HasLinearIO io where
+  constructor MkHasLinearIO
   liftIO1 : (1 _ : IO a) -> io a
 
 public export %inline

libs/prelude/Prelude/Interfaces.idr

@@ -19,6 +19,7 @@ import Prelude.Ops
 |||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
 public export
 interface Semigroup ty where
+  constructor MkSemigroup
   (<+>) : ty -> ty -> ty
 
 ||| Sets equipped with a single binary operation that is associative, along with
@@ -32,6 +33,7 @@ interface Semigroup ty where
 |||     forall a, neutral <+> a == a
 public export
 interface Semigroup ty => Monoid ty where
+  constructor MkMonoid
   neutral : ty
 
 public export
@@ -68,6 +70,7 @@ Monoid b => Monoid (a -> b) where
 ||| @ f a parameterised type
 public export
 interface Functor f where
+  constructor MkFunctor
   ||| Apply a function across everything of type 'a' in a parameterised type
   ||| @ f the parameterised type
   ||| @ func the function to apply
@@ -114,6 +117,7 @@ namespace Functor
 ||| @f The action of the Bifunctor on pairs of objects
 public export
 interface Bifunctor f where
+  constructor MkBifunctor
   ||| The action of the Bifunctor on pairs of morphisms
   |||
   ||| ````idris example
@@ -147,6 +151,7 @@ mapHom f = bimap f f
 
 public export
 interface Functor f => Applicative f where
+  constructor MkApplicative
   pure : a -> f a
   (<*>) : f (a -> b) -> f a -> f b
 
@@ -172,11 +177,13 @@ namespace Applicative
 
 public export
 interface Applicative f => Alternative f where
+  constructor MkAlternative
   empty : f a
   (<|>) : f a -> Lazy (f a) -> f a
 
 public export
 interface Applicative m => Monad m where
+  constructor MkMonad
   ||| Also called `bind`.
   (>>=) : m a -> (a -> m b) -> m b
 
@@ -230,6 +237,7 @@ when False f = pure ()
 ||| @ t The type of the 'Foldable' parameterised type.
 public export
 interface Foldable t where
+  constructor MkFoldable
   ||| Successively combine the elements in a parameterised type using the
   ||| provided function, starting with the element that is in the final position
   ||| i.e. the right-most position.
@@ -385,6 +393,7 @@ namespace Foldable
 ||| Common examples are `Either` and `Pair`.
 public export
 interface Bifoldable p where
+  constructor MkBifoldable
   bifoldr : (a -> acc -> acc) -> (b -> acc -> acc) -> acc -> p a b -> acc
 
   bifoldl : (acc -> a -> acc) -> (acc -> b -> acc) -> acc -> p a b -> acc
@@ -395,6 +404,7 @@ interface Bifoldable p where
 
 public export
 interface (Functor t, Foldable t) => Traversable t where
+  constructor MkTraversable
   ||| Map each element of a structure to a computation, evaluate those
   ||| computations and combine the results.
   traverse : Applicative f => (a -> f b) -> t a -> f (t b)
@@ -411,6 +421,7 @@ for = flip traverse
 
 public export
 interface (Bifunctor p, Bifoldable p) => Bitraversable p where
+  constructor MkBitraversable
   ||| Map each element of a structure to a computation, evaluate those
   ||| computations and combine the results.
   bitraverse : Applicative f => (a -> f c) -> (b -> f d) -> p a b -> f (p c d)

libs/prelude/Prelude/Num.idr

@@ -16,6 +16,7 @@ import Prelude.Ops
 ||| The Num interface defines basic numerical arithmetic.
 public export
 interface Num ty where
+  constructor MkNum
   (+) : ty -> ty -> ty
   (*) : ty -> ty -> ty
   ||| Conversion from Integer.
@@ -26,6 +27,7 @@ interface Num ty where
 ||| The `Neg` interface defines operations on numbers which can be negative.
 public export
 interface Num ty => Neg ty where
+  constructor MkNeg
   ||| The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.
   negate : ty -> ty
   (-) : ty -> ty -> ty
@@ -33,11 +35,13 @@ interface Num ty => Neg ty where
 ||| Numbers for which the absolute value is defined should implement `Abs`.
 public export
 interface Num ty => Abs ty where
+  constructor MkAbs
   ||| Absolute value.
   abs : ty -> ty
 
 public export
 interface Num ty => Fractional ty where
+  constructor MkFractional
   partial
   (/) : ty -> ty -> ty
   partial
@@ -47,6 +51,7 @@ interface Num ty => Fractional ty where
 
 public export
 interface Num ty => Integral ty where
+  constructor MkIntegral
   partial
   div : ty -> ty -> ty
   partial

libs/prelude/Prelude/Show.idr

@@ -41,6 +41,7 @@ Ord Prec where
 ||| Things that have a canonical `String` representation.
 public export
 interface Show ty where
+  constructor MkShow
   ||| Convert a value to its `String` representation.
   ||| @ x the value to convert
   show : (x : ty) -> String

libs/prelude/Prelude/Types.idr

@@ -781,6 +781,7 @@ takeBefore p (x :: xs)
 
 public export
 interface Range a where
+  constructor MkRange
   rangeFromTo : a -> a -> List a
   rangeFromThenTo : a -> a -> a -> List a
 

libs/prelude/Prelude/Uninhabited.idr

@@ -8,6 +8,7 @@ import Prelude.Basics
 ||| A canonical proof that some type is empty.
 public export
 interface Uninhabited t where
+  constructor MkUninhabited
   ||| If I have a t, I've had a contradiction.
   ||| @ t the uninhabited type
   uninhabited : t -> Void

tests/codegen/con001/expected

@@ -2,22 +2,22 @@ Dumping case trees to Main.cases
 prim__add_Integer = [{arg:N}, {arg:N}]: (+Integer [!{arg:N}, !{arg:N}])
 prim__sub_Integer = [{arg:N}, {arg:N}]: (-Integer [!{arg:N}, !{arg:N}])
 prim__mul_Integer = [{arg:N}, {arg:N}]: (*Integer [!{arg:N}, !{arg:N}])
-Main.main = [{ext:N}]: (Prelude.Interfaces.sum [(%con Builtin.MkPair Just 0 [(%con Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [(%lam acc (%lam elem (%lam func (%lam init (%lam input (Prelude.Types.foldr [!func, !init, !input])))))), (%lam elem (%lam acc (%lam func (%lam init (%lam input (Prelude.Types.foldl [!func, !init, !input])))))), (%lam elem (%lam {arg:N} (Prelude.Types.null [!{arg:N}]))), (%lam elem (%lam acc (%lam m (%lam {i_con:N} (%lam funcM (%lam init (%lam input (Prelude.Types.foldlM [!{i_con:N}, !funcM, !init, !input]))))))))]), (%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))])]), (Prelude.Types.rangeFromTo [(%con Builtin.MkPair Just 0 [(%con Prelude.Num.Integral at Prelude/Num.idr:L:C--L:C Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.div [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.mod [!{arg:N}, !{arg:N}])))]), (%con Builtin.MkPair Just 0 [(%con Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%con Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.== [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd./= [!{arg:N}, !{arg:N}])))]), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.compare [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.< [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.> [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.<= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.>= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.max [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.min [!{arg:N}, !{arg:N}])))]), (%con Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (Prelude.Num.negate [!{arg:N}])), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.- [!{arg:N}, !{arg:N}])))])])]), (cast-Integer-Int [1]), (cast-Integer-Int [100])])])
+Main.main = [{ext:N}]: (Prelude.Interfaces.sum [(%con Builtin.MkPair Just 0 [(%con Prelude.Interfaces.MkFoldable Just 0 [(%lam acc (%lam elem (%lam func (%lam init (%lam input (Prelude.Types.foldr [!func, !init, !input])))))), (%lam elem (%lam acc (%lam func (%lam init (%lam input (Prelude.Types.foldl [!func, !init, !input])))))), (%lam elem (%lam {arg:N} (Prelude.Types.null [!{arg:N}]))), (%lam elem (%lam acc (%lam m (%lam {i_con:N} (%lam funcM (%lam init (%lam input (Prelude.Types.foldlM [!{i_con:N}, !funcM, !init, !input]))))))))]), (%con Prelude.Num.MkNum Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))])]), (Prelude.Types.rangeFromTo [(%con Builtin.MkPair Just 0 [(%con Prelude.Num.MkIntegral Just 0 [(%con Prelude.Num.MkNum Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.div [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.mod [!{arg:N}, !{arg:N}])))]), (%con Builtin.MkPair Just 0 [(%con Prelude.EqOrd.MkOrd Just 0 [(%con Prelude.EqOrd.MkEq Just 0 [(%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.== [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd./= [!{arg:N}, !{arg:N}])))]), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.compare [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.< [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.> [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.<= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.>= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.max [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.min [!{arg:N}, !{arg:N}])))]), (%con Prelude.Num.MkNeg Just 0 [(%con Prelude.Num.MkNum Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (Prelude.Num.negate [!{arg:N}])), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.- [!{arg:N}, !{arg:N}])))])])]), (cast-Integer-Int [1]), (cast-Integer-Int [100])])])
 Prelude.Basics.not = [{arg:N}]: (%case !{arg:N} [(%constcase 0 1), (%constcase 1 0)] Nothing)
 Prelude.Basics.flip = [{arg:N}, {arg:N}, {arg:N}]: ((!{arg:N} [!{arg:N}]) [!{arg:N}])
 Builtin.snd = [{arg:N}]: (%case !{arg:N} [(%concase Builtin.MkPair Just 0 [{e:N}, {e:N}] !{e:N})] Nothing)
 Builtin.idris_crash = [{ext:N}]: (crash [___, !{ext:N}])
 Builtin.fst = [{arg:N}]: (%case !{arg:N} [(%concase Builtin.MkPair Just 0 [{e:N}, {e:N}] !{e:N})] Nothing)
 Builtin.believe_me = [{ext:N}]: (believe_me [___, ___, !{ext:N}])
-Prelude.Types.case block in case block in rangeFromTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.takeUntil [(%lam {arg:N} (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [!{arg:N}, (%lam x (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!x]) [(%case (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [1]))] Nothing)]))] Nothing))])])), (%constcase 1 (%con Prelude.Types.:: Just 1 [!{arg:N}, (%con Prelude.Types.Nil Just 0 [])]))] Nothing)
+Prelude.Types.case block in case block in rangeFromTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.takeUntil [(%lam {arg:N} (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.MkOrd Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [!{arg:N}, (%lam x (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.MkNeg Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!x]) [(%case (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.MkNeg Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.MkNum Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [1]))] Nothing)]))] Nothing))])])), (%constcase 1 (%con Prelude.Types.:: Just 1 [!{arg:N}, (%con Prelude.Types.Nil Just 0 [])]))] Nothing)
-Prelude.Types.case block in rangeFromTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.takeUntil [(%lam {arg:N} (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [!{arg:N}, (%lam {arg:N} (%case (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [(%case (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [1]))] Nothing)]))] Nothing))])])), (%constcase 1 (Prelude.Types.case block in case block in rangeFromTo [!{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing)
+Prelude.Types.case block in rangeFromTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.takeUntil [(%lam {arg:N} (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.MkOrd Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [!{arg:N}, (%lam {arg:N} (%case (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.MkNeg Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.MkNum Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [(%case (%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.MkNeg Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.MkNum Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [1]))] Nothing)]))] Nothing))])])), (%constcase 1 (Prelude.Types.case block in case block in rangeFromTo [!{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.MkOrd Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing)
 Prelude.Types.case block in takeUntil = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (%con Prelude.Types.:: Just 1 [!{arg:N}, (%con Prelude.Types.Nil Just 0 [])])), (%constcase 1 (%con Prelude.Types.:: Just 1 [!{arg:N}, (Prelude.Types.takeUntil [!{arg:N}, (%force Inf !{arg:N})])]))] Nothing)
 Prelude.Types.case block in prim__integerToNat = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Builtin.believe_me [!{arg:N}])), (%constcase 1 0)] Nothing)
-Prelude.Types.rangeFromTo = [{arg:N}, {arg:N}, {arg:N}]: (Prelude.Types.case block in rangeFromTo [!{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)])
+Prelude.Types.rangeFromTo = [{arg:N}, {arg:N}, {arg:N}]: (Prelude.Types.case block in rangeFromTo [!{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.EqOrd.MkOrd Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)])
 Prelude.Types.null = [{arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Nil Just 0 [] (%delay Lazy 0)), (%concase Prelude.Types.:: Just 1 [{e:N}, {e:N}] (%delay Lazy 1))] Nothing)
 Prelude.Types.foldr = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Nil Just 0 [] !{arg:N}), (%concase Prelude.Types.:: Just 1 [{e:N}, {e:N}] ((!{arg:N} [!{e:N}]) [(Prelude.Types.foldr [!{arg:N}, !{arg:N}, !{e:N}])]))] Nothing)
 Prelude.Types.foldl = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Nil Just 0 [] !{arg:N}), (%concase Prelude.Types.:: Just 1 [{e:N}, {e:N}] (Prelude.Types.foldl [!{arg:N}, ((!{arg:N} [!{arg:N}]) [!{e:N}]), !{e:N}]))] Nothing)
-Prelude.Types.foldlM = [{arg:N}, {arg:N}, {arg:N}, {ext:N}]: (Prelude.Types.foldl [(%lam ma (%lam b (%case !{arg:N} [(%concase Prelude.Interfaces.Monad at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((((!{e:N} [___]) [___]) [!ma]) [(%lam {eta:N} (Prelude.Basics.flip [!{arg:N}, !b, !{eta:N}]))]))] Nothing))), (%case (%case !{arg:N} [(%concase Prelude.Interfaces.Monad at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [___]) [!{arg:N}]))] Nothing), !{ext:N}])
+Prelude.Types.foldlM = [{arg:N}, {arg:N}, {arg:N}, {ext:N}]: (Prelude.Types.foldl [(%lam ma (%lam b (%case !{arg:N} [(%concase Prelude.Interfaces.MkMonad Just 0 [{e:N}, {e:N}, {e:N}] ((((!{e:N} [___]) [___]) [!ma]) [(%lam {eta:N} (Prelude.Basics.flip [!{arg:N}, !b, !{eta:N}]))]))] Nothing))), (%case (%case !{arg:N} [(%concase Prelude.Interfaces.MkMonad Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Interfaces.MkApplicative Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [___]) [!{arg:N}]))] Nothing), !{ext:N}])
 Prelude.Types.takeUntil = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Stream.:: Just 0 [{e:N}, {e:N}] (Prelude.Types.case block in takeUntil [!{e:N}, !{e:N}, !{arg:N}, (!{arg:N} [!{e:N}])]))] Nothing)
 Prelude.Types.prim__integerToNat = [{arg:N}]: (Prelude.Types.case block in prim__integerToNat [!{arg:N}, (%case (<=Integer [0, !{arg:N}]) [(%constcase 0 1)] Just 0)])
 Prelude.Types.countFrom = [{arg:N}, {arg:N}]: (%con Prelude.Types.Stream.:: Just 0 [!{arg:N}, (%delay Inf (Prelude.Types.countFrom [(!{arg:N} [!{arg:N}]), !{arg:N}]))])
@@ -40,7 +40,7 @@ Prelude.EqOrd.== = [{arg:N}, {arg:N}]: (%case (==Int [!{arg:N}, !{arg:N}]) [(%co
 Prelude.EqOrd.< = [{arg:N}, {arg:N}]: (%case (<Int [!{arg:N}, !{arg:N}]) [(%constcase 0 1)] Just 0)
 Prelude.EqOrd.<= = [{arg:N}, {arg:N}]: (%case (<=Int [!{arg:N}, !{arg:N}]) [(%constcase 0 1)] Just 0)
 Prelude.EqOrd./= = [{arg:N}, {arg:N}]: (Prelude.Basics.not [(Prelude.EqOrd.== [!{arg:N}, !{arg:N}])])
-Prelude.Interfaces.sum = [{arg:N}, {ext:N}]: (%case (Builtin.fst [!{arg:N}]) [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}] (((((!{e:N} [___]) [___]) [(%lam {eta:N} (%lam {clam:N} (%case (Builtin.snd [!{arg:N}]) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{eta:N}]) [!{clam:N}]))] Nothing)))]) [(%case (Builtin.snd [!{arg:N}]) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [0]))] Nothing)]) [!{ext:N}]))] Nothing)
+Prelude.Interfaces.sum = [{arg:N}, {ext:N}]: (%case (Builtin.fst [!{arg:N}]) [(%concase Prelude.Interfaces.MkFoldable Just 0 [{e:N}, {e:N}, {e:N}, {e:N}] (((((!{e:N} [___]) [___]) [(%lam {eta:N} (%lam {clam:N} (%case (Builtin.snd [!{arg:N}]) [(%concase Prelude.Num.MkNum Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{eta:N}]) [!{clam:N}]))] Nothing)))]) [(%case (Builtin.snd [!{arg:N}]) [(%concase Prelude.Num.MkNum Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [0]))] Nothing)]) [!{ext:N}]))] Nothing)
 PrimIO.case block in unsafePerformIO = [{arg:N}, {arg:N}]: (PrimIO.unsafeDestroyWorld [___, !{arg:N}])
 PrimIO.unsafePerformIO = [{arg:N}]: (PrimIO.unsafeCreateWorld [(%lam w (PrimIO.case block in unsafePerformIO [!{arg:N}, (!{arg:N} [!w])]))])
 PrimIO.unsafeDestroyWorld = [{arg:N}, {arg:N}]: !{arg:N}