module Bad-error-message where
postulate
Level : Set
lzero : Level
lsuc : Level → Level
_⊔_ : Level → Level → Level
{-# BUILTIN LEVEL Level #-}
{-# BUILTIN LEVELZERO lzero #-}
{-# BUILTIN LEVELSUC lsuc #-}
{-# BUILTIN LEVELMAX _⊔_ #-}
record R (ℓ : Level) : Set ℓ where
postulate
r : ∀ ℓ → R ℓ
module M (r : ∀ ℓ → R ℓ) where
data D (ℓ : Level) : Set ℓ where
id : ∀ {a} {A : Set a} → A → A
id x = x
data K : Set where
k₁ k₂ : K
P : ∀ {ℓ} → K → Set ℓ → Set ℓ
P k₁ A = A → A
P k₂ A = D _
open M r
postulate
Foo : ∀ {k a} {A : Set a} → P k A → Set
Bar : Set
Bar = Foo M.id
-- Could this error message be improved?
-- Bug.agda:39,11-15
-- Setω is not a valid type.
-- when checking that the expression M.id has type P M.k₁ _34
Original issue reported on code.google.com by nils.anders.danielsson on 28 May 2012 at 9:58
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