record Show (A : Set) : Set where
constructor mkshow
field show : A → String
open Show ⦃ ... ⦄
mutual
show-list·go : ∀ {A} ⦃ sa : Show A ⦄ → List A → String
instance
Show-list : ∀ {A} ⦃ sa : Show A ⦄ → Show (List A)
Show-list = record { show = show-list·go }
show-list·go [] = "[]"
show-list·go (x ∷ xs) = show x <> " ∷ " <> show xs
It looks a bit silly, but it's what my implementation of deriving Show generates for lists. I also think it's perfectly sensible! However, it does not pass termination checking. Since Show is an eta record, the clause compiler translates it to a definition by copatterns:
compiled clauses of Show-list
record
Test141.Show.show ->
done[{_}, ⦃ _ ⦄] Test141.show-list·go {@1} ⦃ @0 ⦄
But if we instead say
Show-list = mkshow show-list·go
then the program is accepted! This is because the clause compiler does not perform copattern translation when the RHS of the definition is a record constructor, only a record expression.
Consider this implementation of
Showfor lists:It looks a bit silly, but it's what my implementation of
deriving Showgenerates for lists. I also think it's perfectly sensible! However, it does not pass termination checking. SinceShowis an eta record, the clause compiler translates it to a definition by copatterns:But if we instead say
then the program is accepted! This is because the clause compiler does not perform copattern translation when the RHS of the definition is a record constructor, only a record expression.