UlfNorell
commented
10 years ago From pumpkingod@gmail.com on May 14, 2012 07:34:19
I think there are two issues here, really. The case splitter for some reason decides that it needs to provide the implicit arguments as patterns to be able to match on monMor (something to do with eta expansion?), which isn't true. And second, because there is no way to match on records with no constructors, we're getting some weird internal representation of the constructor filled in for those implicit patterns.
From pumpkingod@gmail.com on May 10, 2012 21:34:38
On recent Agda:
module Splitting where
record Monoid : Set₁ where field Carrier : Set empty : Carrier times : Carrier → Carrier → Carrier equal : Carrier → Carrier → Set
record MonoidMorphism (M₁ M₂ : Monoid) : Set where constructor monMor module M₁ = Monoid M₁ module M₂ = Monoid M₂ field f : M₁.Carrier → M₂.Carrier .identity : M₂.equal (f M₁.empty) M₂.empty
f : ∀ {M₁ M₂ : Monoid} → MonoidMorphism M₁ M₂ → MonoidMorphism M₁ M₂ f x = {!x!}
case splitting on x in that hole produces this monstrosity:
f {.Splitting.recCon-NOT-PRINTED Carrier empty times equal} {.Splitting.recCon-NOT-PRINTED Carrier₁ empty₁ times₁ equal₁} (monMor f identity) = ?
Original issue: http://code.google.com/p/agda/issues/detail?id=635