has_add

Stream: new members

[Quinn Culver]

Why is my attempt at a has_add instance below failing? The error message at has_add is

type mismatch at application
  has_add f.corge
term
  f.corge
has type
  baz P L f → Type u : Type (u+1)
but is expected to have type
  Type ? : Type (?+1)

MWE attempt:

universe u

variables {P L : Type u}

variables (P L)

inductive foo (P L: Type u)
| points (p : P) : foo
| lines  (l: L) : foo

namespace foo
def bar : Π (x y : foo P L), foo P L
| (points p) (lines l)  :=  sorry
| (points p) (points q) := sorry
| (lines l) (lines m) := sorry
| (lines l) (points p) := sorry

structure baz (f : foo P L) :=
(a b : P)


variables {P L}
def corge (f : foo P L) (my_baz : baz P L f): Type* := {x : P // bar P L (points x)  (points my_baz.a) = bar P L (points my_baz.a) (points my_baz.b) }

instance foo_baz_corge_add (f : foo P L) (my_baz: baz P L f) : has_add (f.corge) := sorry


end foo

[Adam Topaz]

Because has_add X needs X to be a type, and as the error says, f.corge is a function which takes a term of baz … and returns a type.

[Adam Topaz]

You probably want has_add (f.forge my_baz) (untested)

[Eric Wieser]

@Quinn Culver, this seems to be tripping you up over and over again. If you're unsure how to build an expression without errors, you can use #check to slowly assemble it piece by piece to see what's going on.

[Eric Wieser]

Here, that looks like

variables (f : foo P L) (my_baz: baz P L f)

#check f.corge -- reading the type suggests we meant...
#check f.corge my_baz