I don't understand the interactions between records and implicit parameters in . Why can't I manually set the declared implicit parameters of a record's field outside the record's declaration?

@mavaxavou Can you give an example? I don't know what you mean by implicit parameters of a record's field.

@falsifian I'll give it a try. I wanted to define a category. So I defined a record, containing the field object, which is the type of the category's objets. Then a field morphism, which has type object -> object -> Type.

After that, I added a field compose, which build a morphism from two morphisms. It's type is thus compose : {a, b, c : object} -> morphism a b -> morphism b c -> morphism a c.

@falsifian
So far so good, it does what I want. But, if I write a function that takes a category, let's call it cat, and do stuff, I can't manually specify the implicit parameters a, b and c of the function compose cat. Which is ok most of the time, but in rare cases, I would like to be able to specify them.

@mavaxavou Idris or Idris2?

Here's some Idris2 code that seems to do what you're asking for: I can manually specify the implicit parameters for compose:

record Cat where
constructor MkCat
object : Type
morphism : object -> object -> Type
compose : {a, b, c : object} -> morphism a b -> morphism b c -> morphism a c

composeEndomorphism : (c : Cat) -> (o : c.object) -> c.morphism o o -> c.morphism o o -> c.morphism o o
composeEndomorphism c o f g = c.compose {a = o} {b = o} {c = o} f g

@falsifian I'm using Idris 1 for now, but if this works in Idris 2, maybe I should switch to it. Thanks for the help!

@mavaxavou I haven't used Idris 1 in a while. Anyway, not sure if I'm understanding what you're trying to do; LMK.

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!