open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
data D1 : Set where
c : Bool → D1
data D2 : Set where
c : Nat → D2
test : _ → Set
test (c x) = {! !}
test2 : _
test2 = c {! !}
I was rather surprised that Agda does not report an error but only reports some rather cryptic unsolved metavariables:
*All Goals, Errors*
Sort _6
_7 : _6
Sort _8
_9 : _8
_11 : _9
Also both holes report "No type nor action available for hole ?0." when trying to interact with them.
It would be nice if we could give some kind of indication (an error warning?) that the problem is due to the unresolved overloading of the name c.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4