Coercion of Sub-Events in an Effect System

Stream: lean4

[Paul Mure]

I'm trying to implement implicit coercion of sub-events in an algebraic effect system like so:

inductive SumE (ε1 ε2 : Type u → Type v) : Type u → Type v
  | inl {α : Type u} (e1 : ε1 α) : SumE ε1 ε2 α
  | inr {α : Type u} (e2 : ε2 α) : SumE ε1 ε2 α

instance : Add (Type u → Type v) where
  add := SumE

instance : Coe (ε1 α) (SumE ε1 ε2 α) where
  coe e := .inl e

instance : Coe (ε2 α) (SumE ε1 ε2 α) where
  coe e := .inr e

inductive NondetE : Type → Type
  | choose (α : Type) : NondetE α
  | take   (α : Type) : NondetE α

inductive State : Type → Type
  | get : State Nat
  | set (n : Nat) : State Unit

abbrev NDS := NondetE + State

def ndsGet : NDS Nat := .inr State.get

-- This doesn't work
def ndsGetCoe : NDS Nat := Coe.coe State.get

But instance synthesis fails here and I'm not quite sure why.

[Robin Arnez]

I mean, you only have a coercion for SumE and not for +:

inductive SumE (ε1 ε2 : Type u → Type v) : Type u → Type v
  | inl {α : Type u} (e1 : ε1 α) : SumE ε1 ε2 α
  | inr {α : Type u} (e2 : ε2 α) : SumE ε1 ε2 α

instance : Add (Type u → Type v) where
  add := SumE

instance {ε1 ε2 : Type u → Type v} : Coe (ε1 α) ((ε1 + ε2) α) where
  coe e := .inl e

instance {ε1 ε2 : Type u → Type v} : Coe (ε2 α) ((ε1 + ε2) α) where
  coe e := .inr e

inductive NondetE : Type → Type
  | choose (α : Type) : NondetE α
  | take   (α : Type) : NondetE α

inductive State : Type → Type
  | get : State Nat
  | set (n : Nat) : State Unit

abbrev NDS := NondetE + State

def ndsGet : NDS Nat := .inr State.get

def ndsGetCoe : NDS Nat := State.get

Also coercions trigger automatically, no need to Coe.coe (the right thing would be CoeT.coe theoretically)

[Aaron Liu]

Actually Coe.coe andCoeT.coe are almost always wrong since coercions are supposed to be eagerly expanded