[Agda] [newbie] universe levels and BUILTIN EQUALITY

[Andreas Abel]

Thanks, Roman, for the example.

Indeed, big parameters in small data types are believed to be 
consistent, but I do not know of a worked-out theoretical justification. 
(Maybe someone else has pointers for me?!) This is the same for some 
aspects of induction-recursion, or even very-dependent types.

So, far, Agda gives the benefit of the doubt.

Best,
Andreas

On 06.01.2017 00:38, Roman wrote:
> Andreas, it wasn't previously possible to define
>
>     data _≡_ {a} {A : Set a} : A → A → Set where
>       refl : ∀ x → x ≡ x
>
> because this requires forcing of `x` to type check. IIRC, it wasn't
> possible to define
>
>     data _≡_ {a} {A : Set a} (x : A) : A → Set where
>       refl : x ≡ x
>
> either (or was it?). Hence I assumed that both the definitons require
> forcing (which is a poorly documented feature, so I don't really
> know).
>
> But anyway, both the definitions type check currently, so does Agda
> approve something hazardous that should be rejected instead? But if
> Agda justifies this, then how many other hazardous definitions pass
> the type checker as well? Or did I just misunderstand you completely?


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/