git.iko.soy/Idris-dev
on 4c19d46 help sign in
Idris-dev/test/error001/test002.idr
29 lines 493 B history raw
1myid : (a : Type) -> a -> a
2myid _ x = x
4idid : (a : Type) -> a -> a
5idid = myid _ myid
7app : (a -> b) -> a -> b
8app f x = f x
10foo : a -> b -> c -> d -> e -> e
11foo a b c d e = e
13doapp : a -> a
14doapp x = app (myid _) x
16{-
18id : (b : Type k) -> b -> b : Type l, k < l
20foo = id ((a : Type k) -> a -> a) id
21 Type m, k < m
23So we have k < m, k < l, m <= k
25 when converting Type m against Type n, we must have m <= n
26 if we can reach m from n, we have an inconsistency
29 -}