Little typeclass thing

Stream: new members

[Kevin Sullivan]

I notice that the following code works but the following simple replacement breaks it.

Change this code at the end

 let mop := m.op in (mop _ _)

to this seemingly equivalent code

(m.op _ _)

What am I missing here?

import algebra

-- test import
#check has_mul
#check semigroup
#check has_one
#check monoid

namespace alg

universe u

/-
Stack of three typeclasses, each extending from the previous
-/

@[class]
structure my_has_one (α : Type u) :=
(one : α)

/-
has_op
-/

@[class]
structure has_op (α : Type u) :=
(op : α → α → α)


/-
ext_has_op extends from has_op
-/
@[class]
structure ext_has_op (α : Type u) extends has_op α :=
(b : bool)


/-
ext_ext_has_op: optiplicative semigroup plus optiplicative one
-/
@[class]
structure ext_ext_has_op (α : Type u) extends ext_has_op α :=
(s : string)



/-
Instances for nat
-/

@[instance]
def has_one_nat : my_has_one nat := ⟨ 1 ⟩

/-
haz_op nat instance
-/
@[instance]
def has_op_nat : has_op nat := ⟨ nat.mul ⟩


/-
ext_has_op nat instance
-/
instance ext_has_op_nat : ext_has_op nat := ⟨ tt ⟩

/-
ext_ext_has_op nat instance
-/
instance ext_ext_has_op_nat : ext_ext_has_op nat := ⟨ "Hello" ⟩

/-
set_option trace.class_instances true
set_option class.instance_max_depth 20
-/

def mul_foldr
  {α : Type u}
  [m : ext_ext_has_op α]
  [o : my_has_one α]
  :
  list α → α
| [] := o.one
| (h::t) :=
let mop := m.op in
    mop h (mul_foldr t)                     -- Change code here

#eval mul_foldr [1,2,3,4,5]

end alg