metavar resolution going awry in context of universe level function

[UlfNorell]

From sattler....@gmail.com on October 30, 2013 19:37:52

{- Agda development version: Wed Oct 30 16:30:06 GMT 2013

The last line of code triggers the following error, but replacing '_' with 'a' typechecks just fine.

Bug.agda:32,8-11 tt != a of type ⊤ when checking that the expression s _ has type P tt → P a

Changing 'Set (t a)' to 'Set' in line 26 suppresses the error. -}

{-# OPTIONS --without-K #-} module Bug where

postulate Level : Set

{-# BUILTIN LEVEL Level #-}

data ⊤ : Set where tt : ⊤

postulate q : ⊤ → Level P : (a : ⊤) → Set (q a) s : (a : ⊤) → P tt → P a a : ⊤ g : (P tt → P a) → ⊤

v : ⊤ v = g {!!}

Original issue: http://code.google.com/p/agda/issues/detail?id=930

[UlfNorell]

From sattler....@gmail.com on October 30, 2013 11:39:27

The last line should read 'v = g (s _)', please edit the report.

[UlfNorell]

From guillaum...@gmail.com on October 30, 2013 17:31:02

Why do you expect tt to be definitionally equal to a? If you want eta for the unit type, you need to define it as a record:

record ⊤ : Set where constructor tt

[UlfNorell]

From andreas....@gmail.com on October 31, 2013 00:59:26

Well, indeed there is a bug. Agda accepts (s a) at the goal, but not (s ?). That should never happen.

Status: Accepted
Labels: Type-Defect Priority-High Milestone-2.3.4 Meta Level

[UlfNorell]

From andreas....@gmail.com on October 31, 2013 01:31:08

This is what is going on when trying to give (s ?). {-# OPTIONS -v tc.meta:30 -v tc.conv:30 #-}

coerce term v = s ?1 from type t1 = P tt → P ?1 to type t2 = P tt → P a equalSort Set (q tt ⊔ q ?1) == Set (q a ⊔ q tt) compareAtom q tt == q a : Level

-- AS WE CAN SEE, SORT COMPARISON IS BUGGY

compareTerm tt == a : ⊤ sort comparison failed

-- THIS ERROR IS CAUGHT, BUT RETHROWN AT THE END

compareTerm P tt → P ?1 =< P tt → P a : Set (q tt ⊔ q ?1) compare function types t1 = P tt → P ?1 t2 = P tt → P a equalSort Set (q ?1) == Set (q a) compareTerm ?1 == a : ⊤ attempting shortcut ?1 := a solving ?1 := a

-- THIS SOLUTION WOULD ACTUALLY SOLVE THE PROBLEM WITH THE SORTS

Owner: andreas....@gmail.com

[UlfNorell]

From sattler....@gmail.com on October 31, 2013 04:11:56

Guillaume: The code doesn't expect any relationship between tt and a. The expression s a has type P tt → P a, matching the domain of g. Yet, applying g to s _ (or s ?) triggers an error.

Andreas: Cheers for once again tracing the issue that fast!

[UlfNorell]

From andreas....@gmail.com on October 31, 2013 06:46:41

I have a fix for this issue: the sort error should not be thrown when it could be fixed by doing the actual type conversion. But I first want to see if I can improve sort comparison as well to avoid the initial problem...

[UlfNorell]

From andreas....@gmail.com on October 31, 2013 09:30:49

Fixed the buggy sort comparison. If one maximum-term contains a meta, we cannot compare pointwise since we might perform a wrong meta instantiation.

Patch pushed. Thanks for reporting this issue, Christian!

Status: Fixed