MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "HetIdFoolingEta.ma" ---
--- scope checking ---
--- type checking ---
ty-u  Id : ^(A : Set) -> ^(a : A) -> ^(B : Set) -> ^ B -> Set 1
term  Id.refl : .[A : Set] -> .[a : A] -> < Id.refl : Id A a A a >
error during typechecking:
offDia
/// not a type: (f : (A : Set) -> (B : Set) -> (a : A) -> (b : B) -> Id A a B b) -> (A : Set) -> (B : Set) -> (a : A) -> (b : B) -> Id (Id A B a b) (f A B a b) (Id A a A a) (refl A a)
/// inferExpr' (f : (A : Set) -> (B : Set) -> (a : A) -> (b : B) -> Id A a B b) -> (A : Set) -> (B : Set) -> (a : A) -> (b : B) -> Id (Id A B a b) (f A B a b) (Id A a A a) (refl A a)
/// new f : (.[A : Set] -> .[B : Set] -> (a : A) -> (b : B) -> Id A a B b)
/// inferExpr' (A : Set) -> (B : Set) -> (a : A) -> (b : B) -> Id (Id A B a b) (f A B a b) (Id A a A a) (refl A a)
/// new A : Set
/// inferExpr' (B : Set) -> (a : A) -> (b : B) -> Id (Id A B a b) (f A B a b) (Id A a A a) (refl A a)
/// new B : Set
/// inferExpr' (a : A) -> (b : B) -> Id (Id A B a b) (f A B a b) (Id A a A a) (refl A a)
/// new a : v1
/// inferExpr' (b : B) -> Id (Id A B a b) (f A B a b) (Id A a A a) (refl A a)
/// new b : v2
/// inferExpr' Id (Id A B a b) (f A B a b) (Id A a A a) (refl A a)
/// inferExpr' Id (Id A B a b) (f A B a b) (Id A a A a)
/// inferExpr' Id (Id A B a b) (f A B a b)
/// inferExpr' Id (Id A B a b)
/// checkApp (^(A : Set) -> ^(a : A) -> ^(B : Set) -> ^ B -> Set 1) eliminated by Id A B a b
/// inferExpr' Id A B a b
/// inferExpr' Id A B a
/// inferExpr' Id A B
/// checkApp (^(a : v1::Tm) -> ^(B : Set) -> ^ B -> Set 1{A = v1}) eliminated by B
/// leqVal' (subtyping)  < B : Set >  <=+  A
/// leqVal' (subtyping)  Set  <=+  A
/// leqApp: head mismatch Set != A