On 09/01/2019 11.21, Pavel Perikov wrote: > Can anyone explain while declaring inst₂ is prohibited? See the reference manual: https://agda.readthedocs.io/en/latest/language/instance-arguments.html#declaring-instances -- /NAD