1/1: Building Eta (Eta.idr)
Error: While processing right hand side of etaBad. When unifying \x, y => MkTest x y = \x, y => MkTest x y and MkTest = \x, y => MkTest x y.
Mismatch between: Nat and Integer.

Eta:14:10--14:14
 10 | etaGood3: (f : a -> b) -> f = (\x => f x)
 11 | etaGood3 f = Refl
 12 | 
 13 | etaBad : MkTest = (\x : Nat => \y => MkTest ? ?)
 14 | etaBad = Refl
               ^^^^

1/1: Building Eta2 (Eta2.idr)
Error: While processing right hand side of test. When unifying \x => S x = \x => S x and S = \x => S x.
Mismatch between: a and Nat.

Eta2:2:8--2:12
 1 | test : Builtin.Equal S (\x : a => S ?)
 2 | test = Refl
            ^^^^

Error: While processing right hand side of test2. When unifying \x => S x = \x => S x and S = \x => S x.
Mismatch between: a and Nat.

Eta2:5:44--5:48
 1 | test : Builtin.Equal S (\x : a => S ?)
 2 | test = Refl
 3 | 
 4 | test2 : ?
 5 | test2 = {a : _} -> the (S = \x : a => S _) Refl
                                                ^^^^