[Agda] convertibility of implicit and explicit Pi-types

[Jesper Cockx]

Because they are different types? If they were equal, whether a term is
well-typed or not would depend on which order Agda solves constraints,
something that is generally very undesirable. For example, consider the
following program:

```
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

X : Set
explicit : X ≡ (Nat → Nat)
implicit : X ≡ ({Nat} → Nat)

X = _
explicit = refl
implicit = refl

test : (f : X) → Nat
test f = f 42   -- or f {42}?
```

Depending on the order in which Agda checks `explicit` and `implicit`, the
type of `f` will be an explicit or implicit function type, so the user has
to write either `f 42` or `f {42}`. In this case it is still relatively
easy to tell the order in which Agda will check things, but in general
Agda's typechecker relies a lot on postponing and such so the order is not
predictable.

-- Jesper

On Thu, May 21, 2020 at 5:26 PM Thorsten Altenkirch <
Thorsten.Altenkirch at nottingham.ac.uk> wrote:

> Why are implicit and explicit Pi-types not convertible?
>
>
>
> eq : ({_ : Set} → Set) ≡ (Set → Set)
>
> eq = {!refl!}
>
>
>
> {_ : Set} → Set != Set → Set because one is an implicit function
>
> type and the other is an explicit function type
>
> when checking that the expression refl has type
>
> ({_ : Set} → Set) ≡ (Set → Set)
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200521/60eee12f/attachment.html>