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

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