`idris --log 3 heterogenous.idr`

gistfile1.txt

Elaborating {__Infer0}
builtin:0
---> Type a
builtin:0:Constructor {__infer0} : {{A0} : Type} -> ({a0} : {A0}) -> {__Infer0}
Rechecking ({A0} : Type 0) -> {A0} -> {__Infer0}
---> {__infer0} : ({A0} : Type c) -> {A0} -> {__Infer0}
Forced: {__infer0} []
   from ({A0} : Type c) -> {A0} -> {__Infer0}
Elaborating {__Unit0}
builtin:0
---> Type g
builtin:0:Constructor {__II0} : {__Unit0}
Rechecking {__Unit0}
---> {__II0} : {__Unit0}
Forced: {__II0} []
   from {__Unit0}
{__Unit0} collapsible
{__II0} collapsible
Elaborating {__False0}
builtin:0
---> Type i
{__False0} collapsible
Elaborating {__Pair0}
builtin:0
---> Type k -> Type m -> Type o
builtin:0:Constructor {__MkPair0} : {{A0} : Type} -> {{B0} : Type} -> ({a0} : {A0}) -> ({b0} : {B0}) -> {__Pair0} {A0} {B0}
Rechecking ({A0} : Type 0) -> ({B0} : Type 0) -> {A0} -> {B0} -> {__Pair0} {A0} {B0}
---> {__MkPair0} : ({A0} : Type s) -> ({B0} : Type u) -> {A0} -> {B0} -> {__Pair0} {A0} {B0}
Forced: {__MkPair0} [0,1]
   from ({A0} : Type s) -> ({B0} : Type u) -> {A0} -> {B0} -> {__Pair0} {A0} {B0}
Elaborating =
builtin:0
---> ({a0} : Type a1) -> ({b0} : Type c1) -> {a0} -> {b0} -> Type e1
builtin:0:Constructor refl : {{a0} : Type} -> {{x0} : {a0}} -> = {{a0} = _} {{b0} = _} {x0} {x0}
Rechecking ({a0} : Type 0) -> ({x0} : {a0}) -> = {a0} {a0} {x0} {x0}
---> refl : ({a0} : Type k1) -> ({x0} : {a0}) -> = {a0} {a0} {x0} {x0}
Forced: refl [0,1]
   from ({a0} : Type k1) -> ({x0} : {a0}) -> = {a0} {a0} {x0} {x0}
= collapsible
refl collapsible
Loading ibc /Users/tim/.cabal-dev//share/idris-0.9.5.2/base/Prelude.ibc
Loading ibc /Users/tim/.cabal-dev//share/idris-0.9.5.2/base/Builtins.ibc
Loading ibc /Users/tim/.cabal-dev//share/idris-0.9.5.2/base/IO.ibc
Loading ibc /Users/tim/.cabal-dev//share/idris-0.9.5.2/base/Prelude/List.ibc
Already read Builtins
Loading ibc /Users/tim/.cabal-dev//share/idris-0.9.5.2/base/Prelude/Algebra.ibc
Already read Builtins
Loading ibc /Users/tim/.cabal-dev//share/idris-0.9.5.2/base/Prelude/Maybe.ibc
Already read Builtins
Loading ibc /Users/tim/.cabal-dev//share/idris-0.9.5.2/base/Prelude/Nat.ibc
Already read Builtins
Already read Prelude/Algebra
Loading ibc /Users/tim/.cabal-dev//share/idris-0.9.5.2/base/Prelude/Cast.ibc
Already read Prelude/Cast
Already read Prelude/Nat
Loading ibc /Users/tim/.cabal-dev//share/idris-0.9.5.2/base/Prelude/Fin.ibc
Already read Prelude/Nat
Loading ibc /Users/tim/.cabal-dev//share/idris-0.9.5.2/base/Prelude/Either.ibc
Already read Builtins
Already read Prelude/Maybe
Already read Prelude/List
Already read Prelude/List
Already read Prelude/Maybe
Loading ibc /Users/tim/.cabal-dev//share/idris-0.9.5.2/base/Prelude/Monad.ibc
Already read Builtins
Already read Prelude/List
Loading ibc /Users/tim/.cabal-dev//share/idris-0.9.5.2/base/Prelude/Applicative.ibc
Already read Builtins
Loading ibc /Users/tim/.cabal-dev//share/idris-0.9.5.2/base/Prelude/Functor.ibc
Already read Prelude/Applicative
Already read Prelude/Functor
Already read Prelude/Either
Loading ibc /Users/tim/.cabal-dev//share/idris-0.9.5.2/base/Prelude/Vect.ibc
Already read Prelude/Fin
Already read Prelude/List
Already read Prelude/Nat
Loading ibc /Users/tim/.cabal-dev//share/idris-0.9.5.2/base/Prelude/Strings.ibc
Already read Builtins
Already read Prelude/List
Loading ibc /Users/tim/.cabal-dev//share/idris-0.9.5.2/base/Prelude/Chars.ibc
Already read Builtins
Already read Prelude/Cast
Already read Prelude/Either
Already read Prelude/Chars
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 0.9.5.2
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help                

Reading ./heterogenous.idr
namespace {Heterogenous
data Heterogenous.Heterogenous : ({__pi_arg42} : List Type) -> Type where
	Heterogenous.Nil : Heterogenous Nil
	| Heterogenous.:: : {t : Type} -> {ts : List Type} -> (a : t) -> (as : Heterogenous ts) -> Heterogenous (:: t ts)
tydecl Heterogenous.example1 : Heterogenous Nil
pat Heterogenous.example1	Heterogenous.example1 = Nil where []
tydecl Heterogenous.example2 : Heterogenous (:: Nat Nil)
pat Heterogenous.example2	Heterogenous.example2 = :: (the Nat (|fromInteger 0 , 0 , 0L|)) Nil where []
tydecl Heterogenous.example4 : Heterogenous (:: Nat (:: Nat (:: Nat Nil)))
pat Heterogenous.example4	Heterogenous.example4 = :: (the Nat (|fromInteger 1 , 1 , 1L|)) (:: (the Nat (|fromInteger 2 , 2 , 2L|)) (:: (the Nat (|fromInteger 0 , 0 , 0L|)) Nil)) where []
}


[infixr 1 $,infixl 2 <$>,infixl 2 <$,infixl 2 $>,infixl 3 <|>,infixl 4 ||,infixl 4 &&,infixl 5 >>=,infixl 5 /=,infixl 5 ==,infixl 6 <->,infixl 6 <+>,infixl 6 <*>,infixl 6 >=,infixl 6 >,infixl 6 <=,infixl 6 <,infixr 7 ::,infixr 7 ::,infixl 7 >>,infixl 7 <<,infixl 8 ++,infixl 8 -,infixl 8 +,infixl 9 .,infixl 9 /,infixl 9 *]
Type checking ./heterogenous.idr
Elaborating Heterogenous.Heterogenous
heterogenous.idr:3
---> Prelude.List.List Type o1 -> Type q1
heterogenous.idr:4:Constructor Heterogenous.Nil : Heterogenous.Heterogenous (|Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|)
Rechecking Heterogenous.Heterogenous (Prelude.List.Nil Type 0)
---> Heterogenous.Nil : Heterogenous.Heterogenous (Prelude.List.Nil Type t1)
Forced: Heterogenous.Nil []
   from Heterogenous.Heterogenous (Prelude.List.Nil Type t1)
heterogenous.idr:5:Constructor Heterogenous.:: : {t : Type} -> {ts : Prelude.List.List Type} -> (a : t) -> (as : Heterogenous.Heterogenous ts) -> Heterogenous.Heterogenous (|Prelude.List.:: {a = _} t ts , Prelude.Vect.:: {a = _} {n = _} t ts|)
Rechecking (t : Type 0) -> (ts : Prelude.List.List Type 0) -> t -> Heterogenous.Heterogenous ts -> Heterogenous.Heterogenous (Prelude.List.:: Type 0 t ts)
---> Heterogenous.:: : (t : Type v1) -> (ts : Prelude.List.List Type x1) -> t -> Heterogenous.Heterogenous ts -> Heterogenous.Heterogenous (Prelude.List.:: Type z1 t ts)
Forced: Heterogenous.:: [0,1]
   from (t : Type v1) -> (ts : Prelude.List.List Type x1) -> t -> Heterogenous.Heterogenous ts -> Heterogenous.Heterogenous (Prelude.List.:: Type z1 t ts)
Elaborating type decl Heterogenous.example1[]
Heterogenous.example1 pre-type Heterogenous Nil
Heterogenous.example1 type Heterogenous.Heterogenous (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|)
Rechecked to Heterogenous.Heterogenous (Prelude.List.Nil Type f2)
Elaborating clause Heterogenous.example1
Elaborated: Heterogenous.example1
RHS: (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|)
---> Heterogenous.Nil
Must be unreachable:

Against: example1
Optimising patterns
Optimised patterns
CaseDef [] Heterogenous.Nil []
Optimised: CaseDef [] Heterogenous.Nil []
Called names: CGInfo {argsdef = [], calls = [], scg = [], argsused = [], unusedpos = []}
Elaborating type decl Heterogenous.example2[]
Heterogenous.example2 pre-type Heterogenous (:: Nat Nil)
Heterogenous.example2 type Heterogenous.Heterogenous (|Heterogenous.:: {t = _} {ts = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.List.:: {a = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.Vect.:: {a = _} {n = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|)|)
Rechecked to Heterogenous.Heterogenous (Prelude.List.:: Type j2 Prelude.Nat.Nat (Prelude.List.Nil Type l2))
Elaborating clause Heterogenous.example2
Elaborated: Heterogenous.example2
RHS: (|Heterogenous.:: {t = _} {ts = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.List.:: {a = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.Vect.:: {a = _} {n = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|)|)
---> Heterogenous.:: Prelude.Nat.Nat (Prelude.List.Nil Type p2) (Builtins.the Prelude.Nat.Nat (Builtins.fromInteger Prelude.Nat.Nat @Builtins.Num$[Nat] 0)) Heterogenous.Nil
Must be unreachable:

Against: example2
Optimising patterns
Optimised patterns
CaseDef [] Heterogenous.:: Prelude.Nat.Nat (Prelude.List.Nil Type r2) (@Builtins.Num$[Nat].0.Builtins.#!fromInteger.0.#fromInteger' 0 0) Heterogenous.Nil []
Optimised: CaseDef [] Heterogenous.:: (@Builtins.Num$[Nat].0.Builtins.#!fromInteger.0.#fromInteger' 0 0) Heterogenous.Nil []
Called names: CGInfo {argsdef = [], calls = [(@Builtins.Num$[Nat].0.Builtins.#!fromInteger.0.#fromInteger',[[],[]])], scg = [], argsused = [], unusedpos = []}
Elaborating type decl Heterogenous.example4[]
Heterogenous.example4 pre-type Heterogenous (:: Nat (:: Nat (:: Nat Nil)))
Heterogenous.example4 type Heterogenous.Heterogenous (|Heterogenous.:: {t = _} {ts = _} Prelude.Nat.Nat (|Heterogenous.:: {t = _} {ts = _} Prelude.Nat.Nat (|Heterogenous.:: {t = _} {ts = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.List.:: {a = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.Vect.:: {a = _} {n = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|)|) , Prelude.List.:: {a = _} Prelude.Nat.Nat (|Heterogenous.:: {t = _} {ts = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.List.:: {a = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.Vect.:: {a = _} {n = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|)|) , Prelude.Vect.:: {a = _} {n = _} Prelude.Nat.Nat (|Heterogenous.:: {t = _} {ts = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.List.:: {a = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.Vect.:: {a = _} {n = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|)|)|) , Prelude.List.:: {a = _} Prelude.Nat.Nat (|Heterogenous.:: {t = _} {ts = _} Prelude.Nat.Nat (|Heterogenous.:: {t = _} {ts = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.List.:: {a = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.Vect.:: {a = _} {n = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|)|) , Prelude.List.:: {a = _} Prelude.Nat.Nat (|Heterogenous.:: {t = _} {ts = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.List.:: {a = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.Vect.:: {a = _} {n = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|)|) , Prelude.Vect.:: {a = _} {n = _} Prelude.Nat.Nat (|Heterogenous.:: {t = _} {ts = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.List.:: {a = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.Vect.:: {a = _} {n = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|)|)|) , Prelude.Vect.:: {a = _} {n = _} Prelude.Nat.Nat (|Heterogenous.:: {t = _} {ts = _} Prelude.Nat.Nat (|Heterogenous.:: {t = _} {ts = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.List.:: {a = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.Vect.:: {a = _} {n = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|)|) , Prelude.List.:: {a = _} Prelude.Nat.Nat (|Heterogenous.:: {t = _} {ts = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.List.:: {a = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.Vect.:: {a = _} {n = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|)|) , Prelude.Vect.:: {a = _} {n = _} Prelude.Nat.Nat (|Heterogenous.:: {t = _} {ts = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.List.:: {a = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.Vect.:: {a = _} {n = _} Prelude.Nat.Nat (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|)|)|)|)
Rechecked to Heterogenous.Heterogenous (Prelude.List.:: Type t2 Prelude.Nat.Nat (Prelude.List.:: Type v2 Prelude.Nat.Nat (Prelude.List.:: Type x2 Prelude.Nat.Nat (Prelude.List.Nil Type z2))))
Elaborating clause Heterogenous.example4
Elaborated: Heterogenous.example4
RHS: (|Heterogenous.:: {t = _} {ts = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 1 , 1 , 1L|)) (|Heterogenous.:: {t = _} {ts = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 2 , 2 , 2L|)) (|Heterogenous.:: {t = _} {ts = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.List.:: {a = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.Vect.:: {a = _} {n = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|)|) , Prelude.List.:: {a = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 2 , 2 , 2L|)) (|Heterogenous.:: {t = _} {ts = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.List.:: {a = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.Vect.:: {a = _} {n = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|)|) , Prelude.Vect.:: {a = _} {n = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 2 , 2 , 2L|)) (|Heterogenous.:: {t = _} {ts = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.List.:: {a = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.Vect.:: {a = _} {n = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|)|)|) , Prelude.List.:: {a = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 1 , 1 , 1L|)) (|Heterogenous.:: {t = _} {ts = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 2 , 2 , 2L|)) (|Heterogenous.:: {t = _} {ts = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.List.:: {a = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.Vect.:: {a = _} {n = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|)|) , Prelude.List.:: {a = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 2 , 2 , 2L|)) (|Heterogenous.:: {t = _} {ts = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.List.:: {a = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.Vect.:: {a = _} {n = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|)|) , Prelude.Vect.:: {a = _} {n = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 2 , 2 , 2L|)) (|Heterogenous.:: {t = _} {ts = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.List.:: {a = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.Vect.:: {a = _} {n = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|)|)|) , Prelude.Vect.:: {a = _} {n = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 1 , 1 , 1L|)) (|Heterogenous.:: {t = _} {ts = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 2 , 2 , 2L|)) (|Heterogenous.:: {t = _} {ts = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.List.:: {a = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.Vect.:: {a = _} {n = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|)|) , Prelude.List.:: {a = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 2 , 2 , 2L|)) (|Heterogenous.:: {t = _} {ts = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.List.:: {a = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.Vect.:: {a = _} {n = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|)|) , Prelude.Vect.:: {a = _} {n = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 2 , 2 , 2L|)) (|Heterogenous.:: {t = _} {ts = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.List.:: {a = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|) , Prelude.Vect.:: {a = _} {n = _} (Builtins.the Prelude.Nat.Nat (|Builtins.fromInteger {a = _} {{resolvetc}} 0 , 0 , 0L|)) (|Heterogenous.Nil , Prelude.List.Nil {a = _} , Prelude.Vect.Nil {a = _}|)|)|)|)
---> Heterogenous.:: Prelude.Nat.Nat (Prelude.List.:: Type d3 Prelude.Nat.Nat (Prelude.List.:: Type f3 Prelude.Nat.Nat (Prelude.List.Nil Type h3))) (Builtins.the Prelude.Nat.Nat (Builtins.fromInteger Prelude.Nat.Nat @Builtins.Num$[Nat] 1)) (Heterogenous.:: Prelude.Nat.Nat (Prelude.List.:: Type f3 Prelude.Nat.Nat (Prelude.List.Nil Type h3)) (Builtins.the Prelude.Nat.Nat (Builtins.fromInteger Prelude.Nat.Nat @Builtins.Num$[Nat] 2)) (Heterogenous.:: Prelude.Nat.Nat (Prelude.List.Nil Type h3) (Builtins.the Prelude.Nat.Nat (Builtins.fromInteger Prelude.Nat.Nat @Builtins.Num$[Nat] 0)) Heterogenous.Nil))
Must be unreachable:

Against: example4
Optimising patterns
Optimised patterns
CaseDef [] Heterogenous.:: Prelude.Nat.Nat (Prelude.List.:: Type j3 Prelude.Nat.Nat (Prelude.List.:: Type l3 Prelude.Nat.Nat (Prelude.List.Nil Type n3))) (@Builtins.Num$[Nat].0.Builtins.#!fromInteger.0.#fromInteger' 1 1) (Heterogenous.:: Prelude.Nat.Nat (Prelude.List.:: Type p3 Prelude.Nat.Nat (Prelude.List.Nil Type r3)) (@Builtins.Num$[Nat].0.Builtins.#!fromInteger.0.#fromInteger' 2 2) (Heterogenous.:: Prelude.Nat.Nat (Prelude.List.Nil Type t3) (@Builtins.Num$[Nat].0.Builtins.#!fromInteger.0.#fromInteger' 0 0) Heterogenous.Nil)) []
Optimised: CaseDef [] Heterogenous.:: (@Builtins.Num$[Nat].0.Builtins.#!fromInteger.0.#fromInteger' 1 1) (Heterogenous.:: (@Builtins.Num$[Nat].0.Builtins.#!fromInteger.0.#fromInteger' 2 2) (Heterogenous.:: (@Builtins.Num$[Nat].0.Builtins.#!fromInteger.0.#fromInteger' 0 0) Heterogenous.Nil)) []
Called names: CGInfo {argsdef = [], calls = [(@Builtins.Num$[Nat].0.Builtins.#!fromInteger.0.#fromInteger',[[],[]])], scg = [], argsused = [], unusedpos = []}
Totality checking
Checking Heterogenous.example1 for totality
Paths for Heterogenous.example1 yield [not yet checked for totality]
Checking Heterogenous.example2 for totality
Paths for Heterogenous.example2 yield [not yet checked for totality,Total,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality]
Checking Heterogenous.example4 for totality
Paths for Heterogenous.example4 yield [not yet checked for totality,Total,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality,not yet checked for totality]
Finished ./heterogenous.idr
Universe checking
user interrupt