OpClassesRepro.idr

module OpClassesRepro

record SemigroupRec (t : Type) (op : t -> t -> t) where
    constructor SemigroupInfo
    associative : (a : t) -> (b : t) -> (c : t) -> (op (op a b) c = op a (op b c))
    
resolveSemigroup
  :  {auto associative : (a : t) -> (b : t) -> (c : t) -> (op (op a b) c = op a (op b c))} 
  -> SemigroupRec t op
resolveSemigroup {associative} = SemigroupInfo associative

%hint
addAssoc
  : (a : Nat) -> (b : Nat) -> (c : Nat) -> plus (plus a b) c = plus a (plus b c)
addAssoc a b c = sym (plusAssociative a b c)

%hint
create : SemigroupRec Nat Prelude.Nat.plus
create = resolveSemigroup

When I try to load this file, I get the following error:

- + Errors (1)
 `-- op-classes-repro.idr line 20 col 9:
     When checking right hand side of create with expected type
             SemigroupRec Nat plus
     
     When checking argument associative to function OpClassesRepro.resolveSemigroup:
             Can't find a value of type 
                     (a : Nat) ->
                     (b : Nat) -> (c : Nat) -> plus (plus a b) c = plus a (plus b c)

but, why can’t resolveSemigroup find addAssoc, which has exactly that type?

Now @srdqty got it working by changing the associative parameters to be implicit.

module OpClassesRepro

record SemigroupRec (t : Type) (op : t -> t -> t) where
    constructor SemigroupInfo
    associative : {a : t} -> {b : t} -> {c : t} -> (op (op a b) c = op a (op b c))

resolveSemigroup
  :  {auto associative : {a : t} -> {b : t} -> {c : t} -> (op (op a b) c = op a (op b c))}
  -> SemigroupRec t op
resolveSemigroup {associative} = SemigroupInfo associative

%hint
addAssoc
  : {a : Nat} -> {b : Nat} -> {c : Nat} -> plus (plus a b) c = plus a (plus b c)
addAssoc {a} {b} {c} = sym (plusAssociative a b c)

%hint
create : SemigroupRec Nat Prelude.Nat.plus
create = resolveSemigroup

But when I try to pull out that associative definition

module OpClassesRepro

Associative : (t -> t -> t) -> Type
Associative {t} op = {a : t} -> {b : t} -> {c : t} -> (op (op a b) c = op a (op b c))

record SemigroupRec (t : Type) (op : t -> t -> t) where
    constructor SemigroupInfo
    associative : Associative op

resolveSemigroup
  :  {auto associative : Associative op}
  -> SemigroupRec t op
resolveSemigroup {associative} = SemigroupInfo associative

%hint
addAssoc : Associative Prelude.Nat.plus
addAssoc {a} {b} {c} = sym (plusAssociative a b c)

%hint
create : SemigroupRec Nat Prelude.Nat.plus
create = resolveSemigroup

I now get a new error:

- + Errors (2)
 |-- builtin line 0 col -1:
 |   When checking left hand side of addAssoc:
 |   Type mismatch between
 |           plus (plus a b) c = plus a (plus b c) (Type of addAssoc a b c)
 |   and
 |           _ -> _ (Is addAssoc a b c applied to too many arguments?)
 |   
 |   Specifically:
 |           Type mismatch between
 |                   (=) plus (plus a b) c
 |           and
 |                   \uv => _ -> uv
 `-- op-classes-repro2.idr line 21 col 9:
     When checking right hand side of create with expected type
             SemigroupRec Nat plus
     
     When checking argument associative to function OpClassesRepro.resolveSemigroup:
             Can't find a value of type 
                     plus (plus a b1) c1 = plus a (plus b1 c1)

I’m guessing it’s because the a b and c don’t exist syntactically in the type, since if I replace that one line with addAssoc : {a : Nat} -> {b : Nat} -> {c : Nat} -> (plus (plus a b) c = plus a (plus b c)) everything works again.

So I did something similar to what I did here: https://github.com/srdqty/idris-noteq/blob/master/src/Decidable/Equality/NotEq.idr

Which is define a new datatype for the property instead of trying to just use an alias. I think that auto doesn't even try to find function types and that's why the functions without implicit arguments were failing.

Idris accepted the following:

module OpClassesRepro

%default total

data Associative : (t -> t -> t) -> Type where
  MkAssociative : ({a : t} -> {b : t} -> {c : t} -> (op (op a b) c = op a (op b c)))
               -> Associative op

record SemigroupRec (t : Type) (op : t -> t -> t) where
    constructor SemigroupInfo
    associative : Associative op

resolveSemigroup
  :  {auto associative : Associative op}
  -> SemigroupRec t op
resolveSemigroup {associative} = SemigroupInfo associative

plusAssociative' : {left : Nat} -> left + (centre + right) = left + centre + right
plusAssociative' {left} {centre} {right} = plusAssociative left centre right

%hint
addAssoc : Associative Prelude.Nat.plus
addAssoc = MkAssociative (sym plusAssociative')

%hint
create : SemigroupRec Nat Prelude.Nat.plus
create = resolveSemigroup

I also tried the following, but it didn't work:

module OpClassesRepro

Associative : {op: t -> t -> t} -> Type
Associative {t} {op} = {a : t} -> {b : t} -> {c : t} -> (op (op a b) c = op a (op b c))

record SemigroupRec (t : Type) (op : t -> t -> t) where
    constructor SemigroupInfo
    associative : Associative {op=op}

resolveSemigroup
  :  {op : t -> t -> t}
  -> {auto associative : Associative {op=op}}
  -> SemigroupRec t op
resolveSemigroup {associative} = SemigroupInfo associative

plusAssociative' : {left : Nat} -> left + (centre + right) = left + centre + right
plusAssociative' {left} {centre} {right} = plusAssociative left centre right

%hint
addAssoc : Associative {op=Prelude.Nat.plus}
addAssoc = sym plusAssociative'

%hint
create : SemigroupRec Nat Prelude.Nat.plus
create = resolveSemigroup