gistfile1.txt

     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 0.9.18-
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help               

Idris is free software with ABSOLUTELY NO WARRANTY.            
For details type :warranty.
Type checking ./test.idr
Elaborating type decl Main.forwards[]
Main.forwards pre-type Profunctor p =>
(__pi_arg : Iso {p = p}
s
t
a
b) ->
(__pi_arg : s) ->
a[]
Main.forwards type pre-addimpl {p : _} ->
{s : _} ->
{t : _} ->
{a : _} ->
{b : _} ->
Profunctor p =>
(__pi_arg : Iso {p = p}
s
t
a
b) ->
(__pi_arg : s) ->
a
Main.forwards type []
{p : _} ->
{s : _} ->
{t : _} ->
{a : _} ->
{b : _} ->
Main.Profunctor p =>
(__pi_arg : Main.Iso {p = p}
{{%instance}}
s
t
a
b) ->
(__pi_arg7 : s) ->
a
Profunctor p => Iso s t a b -> s -> a
Elaborated: (p : Type 0 -> Type 0 -> Type 0) -> (s : Type 0) -> (t : Type 0) -> (a : Type 0) -> (b : Type 0) -> ({constrarg0} : Main.Profunctor p) -> Main.Iso p {constrarg0} s t a b -> s -> a
Rechecking
Main.forwards: inaccessible arguments: [(0,p),(1,s),(2,t),(3,a),(4,b)] from (p : Type k48 -> Type n48 -> Type q48) -> (s : Type t48) -> (t : Type w48) -> (a : Type z48) -> (b : Type c49) -> ({constrarg0} : Main.Profunctor p) -> Main.Iso p {constrarg0} s t a b -> s -> a
{p : _} ->
{s : _} ->
{t : _} ->
{a : _} ->
{b : _} ->
Main.Profunctor p =>
(__pi_arg : Main.Iso {p = p}
{{%instance}}
s
t
a
b) ->
(__pi_arg7 : s) ->
a
Implicit Main.forwards [PImp {priority = 0, machine_inf = True, argopts = [], pname = p, getTm = _},PImp {priority = 0, machine_inf = True, argopts = [], pname = s, getTm = _},PImp {priority = 0, machine_inf = True, argopts = [], pname = t, getTm = _},PImp {priority = 0, machine_inf = True, argopts = [], pname = a, getTm = _},PImp {priority = 0, machine_inf = True, argopts = [], pname = b, getTm = _},PConstraint {priority = 10, argopts = [], pname = {constrarg0}, getTm = Profunctor p},PExp {priority = 1, argopts = [], pname = __pi_arg, getTm = Iso s t a b},PExp {priority = 1, argopts = [], pname = __pi_arg7, getTm = s}]
Statics for Main.forwards (p : Type k48 -> Type n48 -> Type q48) -> (s : Type t48) -> (t : Type w48) -> (a : Type z48) -> (b : Type c49) -> ({constrarg0} : Main.Profunctor p) -> Main.Iso p {constrarg0} s t a b -> s -> a
{p : _} ->
{s : _} ->
{t : _} ->
{a : _} ->
{b : _} ->
Main.Profunctor p =>
(__pi_arg : Main.Iso {p = p}
{{%instance}}
s
t
a
b) ->
(__pi_arg7 : s) ->
a
[({constrarg0},Main.Profunctor p)]
[(p,Type k48 -> Type n48 -> Type q48),(s,Type t48),(t,Type w48),(a,Type z48),(b,Type c49),(__pi_arg,Main.Iso p {constrarg0} s t a b),(__pi_arg7,s)]
[p]
[True,False,False,False,False,True,False,False]
Rechecked to (p : Type k48 -> Type n48 -> Type q48) -> (s : Type t48) -> (t : Type w48) -> (a : Type z48) -> (b : Type c49) -> ({constrarg0} : Main.Profunctor p) -> Main.Iso p {constrarg0} s t a b -> s -> a
Rechecked to (p : Type k48 -> Type n48 -> Type q48) -> (s : Type t48) -> (t : Type w48) -> (a : Type z48) -> (b : Type c49) -> Main.Profunctor p -> (p a b -> p s t) -> s -> a
Elaborating clause Main.forwards
LHS: test.idr:24:10 Main.forwards {p = _}
{s = s}
{t = t}
{a = a}
{b = b}
{{%instance}}
i
Fixed parameters: [] from forwards i
((p : Type i49 -> Type l49 -> Type o49) -> (s : Type r49) -> (t : Type u49) -> (a : Type x49) -> (b : Type a50) -> (constrarg : Main.Profunctor p) -> Main.Iso p constrarg s t a b -> s -> a,[PImp {priority = 0, machine_inf = True, argopts = [], pname = p, getTm = _},PImp {priority = 0, machine_inf = True, argopts = [], pname = s, getTm = _},PImp {priority = 0, machine_inf = True, argopts = [], pname = t, getTm = _},PImp {priority = 0, machine_inf = True, argopts = [], pname = a, getTm = _},PImp {priority = 0, machine_inf = True, argopts = [], pname = b, getTm = _},PConstraint {priority = 10, argopts = [], pname = {constrarg0}, getTm = Profunctor p},PExp {priority = 1, argopts = [], pname = __pi_arg, getTm = Iso s t a b},PExp {priority = 1, argopts = [], pname = __pi_arg7, getTm = s}])
Elaborated: pat s : Type 0. pat t : Type 0. pat a : Type 0. pat b : Type 0. pat {p505} : Type 0 -> Type 0 -> Type 0. pat {constrarg510} : Main.Profunctor {p505}. pat i : Main.Iso {p505} {constrarg510} s t a b. Main.forwards {p505} s t a b {constrarg510} i
Elaborated type: pty s : Type 0. pty t : Type 0. pty a : Type 0. pty b : Type 0. pty {p505} : Type 0 -> Type 0 -> Type 0. pty {constrarg510} : Main.Profunctor {p505}. pty i : Main.Iso {p505} {constrarg510} s t a b. s -> a
Injective: Main.forwards [{p505},{p504}]
Normalised LHS: Main.forwards {p = p}
{s = s}
{t = t}
{a = a}
{b = b}
{{constrarg}}
i
Checked pat s : Type g50. pat t : Type i50. pat a : Type k50. pat b : Type m50. pat {p505} : Type o50 -> Type r50 -> Type u50. pat {constrarg510} : Main.Profunctor {p505}. pat i : {p505} a b -> {p505} s t. Main.forwards {p505} s t a b {constrarg510} i
pty s : Type g50. pty t : Type i50. pty a : Type k50. pty b : Type m50. pty {p505} : Type o50 -> Type r50 -> Type u50. pty {constrarg510} : Main.Profunctor {p505}. pty i : Main.Iso {p505} {constrarg510} s t a b. s -> a
Where block:
 [tydecl Main.forwards:fi:0 : (s : Type) -> (t : Type) -> (a : Type) -> (b : Type) -> (p : (__pi_arg : Type) -> (__pi_arg2 : Type) -> Type) [static] -> (constrarg : Main.Profunctor p) [static] -> (i : Main.Iso {p = p} {{constrarg}} s t a b) -> (__pi_arg : Forgotten a a b) -> Forgotten a s t,pat Main.forwards:fi:0 	   Main.forwards, fi s t a b p constrarg i  = specialize i where []]
[]
Elaborating type decl Main.forwards, fi[]
Main.forwards, fi pre-type (s : Type) ->
(t : Type) ->
(a : Type) ->
(b : Type) ->
(p : (__pi_arg : Type) ->
(__pi_arg2 : Type) ->
Type) [static] ->
(constrarg : Main.Profunctor p) [static] ->
(i : Main.Iso {p = p}
{{constrarg}}
s
t
a
b) ->
(__pi_arg : Forgotten a
a
b) ->
Forgotten a
s
t[]
Main.forwards, fi type pre-addimpl (s : Type) ->
(t : Type) ->
(a : Type) ->
(b : Type) ->
(p : (__pi_arg : Type) ->
(__pi_arg2 : Type) ->
Type) [static] ->
(constrarg : Main.Profunctor p) [static] ->
(i : Main.Iso {p = p}
{{constrarg}}
s
t
a
b) ->
(__pi_arg : Forgotten a
a
b) ->
Forgotten a
s
t
Main.forwards, fi type []
(s : Type) ->
(t : Type) ->
(a : Type) ->
(b : Type) ->
(p : (__pi_arg : Type) ->
(__pi_arg2 : Type) ->
Type) [static] ->
(constrarg : Main.Profunctor p) [static] ->
(i : Main.Iso {p = p}
{{constrarg}}
s
t
a
b) ->
(__pi_arg9 : Main.Forgotten a
a
b) ->
Main.Forgotten a
s
t
(s : Type) -> (t : Type) -> (a : Type) -> (b : Type) -> (p : Type -> Type -> Type) [static] -> (constrarg : Profunctor p) [static] -> Iso s t a b -> Forgotten a a b -> Forgotten a s t
Elaborated: (s : Type 0) -> (t : Type 0) -> (a : Type 0) -> (b : Type 0) -> ({p505} : Type 0 -> Type 0 -> Type 0) -> ({constrarg510} : Main.Profunctor {p505}) -> Main.Iso {p505} {constrarg510} s t a b -> Main.Forgotten a a b -> Main.Forgotten a s t
Rechecking
Main.forwards, fi: inaccessible arguments: [] from (s : Type w50) -> (t : Type z50) -> (a : Type c51) -> (b : Type f51) -> ({p505} : Type i51 -> Type l51 -> Type o51) -> ({constrarg510} : Main.Profunctor {p505}) -> Main.Iso {p505} {constrarg510} s t a b -> Main.Forgotten a a b -> Main.Forgotten a s t
(s : Type) ->
(t : Type) ->
(a : Type) ->
(b : Type) ->
(p : (__pi_arg : Type) ->
(__pi_arg2 : Type) ->
Type) [static] ->
(constrarg : Main.Profunctor p) [static] ->
(i : Main.Iso {p = p}
{{constrarg}}
s
t
a
b) ->
(__pi_arg9 : Main.Forgotten a
a
b) ->
Main.Forgotten a
s
t
Implicit Main.forwards, fi [PExp {priority = 1, argopts = [], pname = s, getTm = Type},PExp {priority = 1, argopts = [], pname = t, getTm = Type},PExp {priority = 1, argopts = [], pname = a, getTm = Type},PExp {priority = 1, argopts = [], pname = b, getTm = Type},PExp {priority = 1, argopts = [], pname = {p505}, getTm = Type -> Type -> Type},PExp {priority = 1, argopts = [], pname = {constrarg510}, getTm = Profunctor p},PExp {priority = 1, argopts = [], pname = i, getTm = Iso s t a b},PExp {priority = 1, argopts = [], pname = __pi_arg9, getTm = Forgotten a a b}]
Statics for Main.forwards, fi (s : Type w50) -> (t : Type z50) -> (a : Type c51) -> (b : Type f51) -> ({p505} : Type i51 -> Type l51 -> Type o51) -> ({constrarg510} : Main.Profunctor {p505}) -> Main.Iso {p505} {constrarg510} s t a b -> Main.Forgotten a a b -> Main.Forgotten a s t
(s : Type) ->
(t : Type) ->
(a : Type) ->
(b : Type) ->
(p : (__pi_arg : Type) ->
(__pi_arg2 : Type) ->
Type) [static] ->
(constrarg : Main.Profunctor p) [static] ->
(i : Main.Iso {p = p}
{{constrarg}}
s
t
a
b) ->
(__pi_arg9 : Main.Forgotten a
a
b) ->
Main.Forgotten a
s
t
[({p505},Type i51 -> Type l51 -> Type o51),({constrarg510},Main.Profunctor {p505})]
[(s,Type w50),(t,Type z50),(a,Type c51),(b,Type f51),(i,Main.Iso {p505} {constrarg510} s t a b),(__pi_arg9,Main.Forgotten a a b)]
[{p505}]
[False,False,False,False,True,True,False,False]
Rechecked to (s : Type w50) -> (t : Type z50) -> (a : Type c51) -> (b : Type f51) -> ({p505} : Type i51 -> Type l51 -> Type o51) -> ({constrarg510} : Main.Profunctor {p505}) -> Main.Iso {p505} {constrarg510} s t a b -> Main.Forgotten a a b -> Main.Forgotten a s t
Rechecked to (s : Type w50) -> (t : Type z50) -> (a : Type c51) -> (b : Type f51) -> ({p505} : Type i51 -> Type l51 -> Type o51) -> Main.Profunctor {p505} -> ({p505} a b -> {p505} s t) -> Main.Forgotten a a b -> Main.Forgotten a s t
Elaborating clause Main.forwards, fi
LHS: test.idr:26:6 Main.forwards, fi s
t
a
b
{ p 505 }
{ constrarg 510 }
i
Fixed parameters: [] from Main.forwards, fi s t a b p constrarg i
((s : Type u51) -> (t : Type x51) -> (a : Type a52) -> (b : Type d52) -> (p : Type g52 -> Type j52 -> Type m52) -> (constrarg : Main.Profunctor p) -> Main.Iso p constrarg s t a b -> Main.Forgotten a a b -> Main.Forgotten a s t,[PExp {priority = 1, argopts = [], pname = s, getTm = Type},PExp {priority = 1, argopts = [], pname = t, getTm = Type},PExp {priority = 1, argopts = [], pname = a, getTm = Type},PExp {priority = 1, argopts = [], pname = b, getTm = Type},PExp {priority = 1, argopts = [], pname = {p505}, getTm = Type -> Type -> Type},PExp {priority = 1, argopts = [], pname = {constrarg510}, getTm = Profunctor p},PExp {priority = 1, argopts = [], pname = i, getTm = Iso s t a b},PExp {priority = 1, argopts = [], pname = __pi_arg9, getTm = Forgotten a a b}])
Elaborated: pat s : Type 0. pat t : Type 0. pat a : Type 0. pat b : Type 0. pat {p505} : Type 0 -> Type 0 -> Type 0. pat {constrarg510} : Main.Profunctor {p505}. pat i : Main.Iso {p505} {constrarg510} s t a b. Main.forwards, fi s t a b {p505} {constrarg510} i
Elaborated type: pty s : Type 0. pty t : Type 0. pty a : Type 0. pty b : Type 0. pty {p505} : Type 0 -> Type 0 -> Type 0. pty {constrarg510} : Main.Profunctor {p505}. pty i : Main.Iso {p505} {constrarg510} s t a b. Main.Forgotten a a b -> Main.Forgotten a s t
Injective: Main.forwards, fi [{p505},{p1017}]
Normalised LHS: Main.forwards, fi s
t
a
b
p
constrarg
i
Checked pat s : Type s52. pat t : Type u52. pat a : Type w52. pat b : Type y52. pat {p505} : Type a53 -> Type d53 -> Type g53. pat {constrarg510} : Main.Profunctor {p505}. pat i : {p505} a b -> {p505} s t. Main.forwards, fi s t a b {p505} {constrarg510} i
pty s : Type s52. pty t : Type u52. pty a : Type w52. pty b : Type y52. pty {p505} : Type a53 -> Type d53 -> Type g53. pty {constrarg510} : Main.Profunctor {p505}. pty i : Main.Iso {p505} {constrarg510} s t a b. Main.Forgotten a a b -> Main.Forgotten a s t
Where block:
 []
[]
specialize i
RHS: [s,t,a,b,{p505},{constrarg510},i] Main.specialize {q = _}
{a = _}
{b = _}
{s = _}
{t = _}
{{%instance}}
i
STARTING CHECK