Bad error message: "Setω is not a valid type"

[UlfNorell]

From nils.anders.danielsson on May 28, 2012 11:58:47

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: http://code.google.com/p/agda/issues/detail?id=659

[UlfNorell]

From andreas....@gmail.com on May 31, 2012 03:49:35

The story here is:

compareType _34 =< ((ℓ : Level) → R ℓ) sorts: (Set _33) and Setω term _33 := Setω MetaVars.assign: assigning to Sort Inf sort comparison failed s1 = (Set _33) s2 = Setω compareTerm _34 =< ((ℓ : Level) → R ℓ) : (Set _33) attempting shortcut _34 := ((ℓ : Level) → R ℓ) ...

and the respective code in Conversion.hs

compareSort CmpEq s1 s2 `catchError` \err -> case err of
      TypeError _ _ -> do
        reportSDoc "tc.conv.type" 30 $ vcat
          [ text "sort comparison failed"
          , nest 2 $ vcat
            [ text "s1 =" <+> prettyTCM s1
            , text "s2 =" <+> prettyTCM s2
            ]
          ]
        -- This error will probably be more informative
        compareTerm cmp (sort s1) a1 a2
        -- Throw the original error if the above doesn't
        -- give an error (for instance, due to pending
        -- constraints).
        -- Or just ignore it... We run into this with irrelevant levels
        -- which may show up in sort constraints, causing them to fail.
        -- In any case it's not safe to ignore the error, for instance
        -- a1 might be Set and a2 a meta of type Set, in which case we
        -- really need the sort comparison to fail, instead of silently
        -- instantiating the meta.
        throwError err

When sort comparison creates a universe inconsistency, Agda tries to produce a better error message by invoking the term comparison. This does not produce an error in this case, so the non-informative error is thrown. Maybe it could be extended to include the two terms which were tried to match, like:

a1 != a2 because of err

Cc: andreas....@gmail.com
Labels: Errors

[UlfNorell]

From andreas....@gmail.com on May 31, 2012 05:57:24

I have changed the error message to

((r₁ : (ℓ : Level) → R ℓ) {a : Level} {A : Set a} → A → A) !=< (P {_33} _32 _34) because this would result in an invalid use of Setω when checking that the expression M.id has type (P {_33} _32 _34)

I hope that is better.

[UlfNorell]

From andreas....@gmail.com on May 31, 2012 06:00:56

Status: Fixed
Owner: andreas....@gmail.com
Cc: -andreas....@gmail.com

[UlfNorell]

From p.giarrusso on July 23, 2013 09:21:19

Could the error message mention level-polymorphism and provide a link? You can mention Setω if you like, but if would be helpful to give some rationale such as

"Types of level-polymorphic functions don't have a type"

(Maybe you want universe-polymorphic there instead, but level-polymorphic is IMHO clearer since Level often appears in Agda source). A link to the Agda wiki would also help - it could at least link to some ML discussion (or paste its contents), such as http://comments.gmane.org/gmane.comp.lang.agda/5339

[UlfNorell]

From nils.anders.danielsson on August 21, 2013 08:45:11

Types of level-polymorphic functions can have types:

data D (ℓ : Level) : Set where d : D ℓ

Type-of-foo : Set Type-of-foo = (ℓ : Level) → D ℓ

foo : Type-of-foo foo _ = d

Status: Accepted
Labels: -Errors ErrorReporting Priority-Medium