test: for issue #439

closes #439

tests/lean/439.lean

@@ -0,0 +1,39 @@
+universe u
+
+structure Fn (E I : Sort u) := (exp : E) (imp : I)
+instance (E I : Sort u) :  CoeFun (Fn E I) (fun _ => I) := {coe := fun K => K.imp}
+
+class Bar.{w} (P : Sort u) :=
+  fn : P -> Sort w
+
+variable {P : Sort u} (B : Bar P)
+variable (fn : Fn ((p : P) -> B.fn p) ({p : P} -> B.fn p))
+#check coeFun fn -- Result is as expected (implicit)
+/-
+  fn : {p : P} → Bar.fn p
+-/
+
+variable (p : P)
+variable (Bp : Bar.fn p)
+#check fn Bp
+/-
+application type mismatch
+  Fn.imp fn Bp
+argument
+  Bp
+has type
+  Bar.fn p : Sort ?u.635
+but is expected to have type
+  P : Sort u
+-/
+#check fn p
+#check fn (p := p)
+
+
+variable (fn' : Fn ((p : P) -> B.fn p -> B.fn p) ({p : P} -> B.fn p -> B.fn p))
+
+-- Expect no error
+#check fn' Bp
+
+-- Expect error
+#check fn' p

tests/lean/439.lean.expected.out

@@ -0,0 +1,19 @@
+fn : {p : P} → Bar.fn p
+439.lean:18:7-18:12: error: function expected at
+  Fn.imp fn ?m
+term has type
+  Bar.fn ?m
+439.lean:29:7-29:11: error: function expected at
+  Fn.imp fn ?m
+term has type
+  Bar.fn ?m
+Fn.imp fn p : Bar.fn p
+Fn.imp fn' p Bp : Bar.fn p
+439.lean:39:7-39:12: error: application type mismatch
+  Fn.imp fn' ?m p
+argument
+  p
+has type
+  P : Sort u
+but is expected to have type
+  Bar.fn ?m : Sort ?u