New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Disambiguation of type based on pattern leads to non-unique meta solution #2834

Closed
jespercockx opened this Issue Nov 3, 2017 · 3 comments

Comments

@jespercockx
Contributor

jespercockx commented Nov 3, 2017

In the following example, Agda instantiates X to Bool, even though it could equally well be instantiated with A instead.

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

test : (A : Set) (let X = _) (x : X) (p : A ≡ Bool)  Bool
test .Bool true  refl = false
test .Bool false refl = true
@andreasabel

This comment has been minimized.

Contributor

andreasabel commented Nov 6, 2017

This does not look scary, can you make the case scarier?

@jespercockx

This comment has been minimized.

Contributor

jespercockx commented Nov 6, 2017

Halloween is over, but I can try. This code is rejected:

{-# OPTIONS --without-K #-}

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

test : (A : Set) (let X = {!!}) (x : X) (p : X ≡ Bool)  Bool
test .Bool true  refl = false
test .Bool false refl = true

but simply filling in the hole with A causes it to be accepted. Scary enough? 👻👻👻

@andreasabel

This comment has been minimized.

Contributor

andreasabel commented Nov 6, 2017

Ok, good enough. I still do not tremble. ;-)

jespercockx added a commit to jespercockx/agda that referenced this issue Dec 11, 2017

[ new ] Big refactoring of the LHS checker
This (partially) reimplements the algorithm for checking left-hand sides.

- In patterns, dot pattern instantiations, absurd patterns, as patterns, etc. are treated uniformly as "problem equations" between an abstract pattern and an internal term.
- Internal patterns now carry "pattern origin" tags to remember what pattern was originally written by the user. This gives a much more robust way to print patterns as the user wrote them.
- The new implementation is much more flexible with regards to the placement of dot patterns. In particular, variables never require a dot anymore (see test/Succeed/Issue473-1606.agda).
- Case splitting is no longer allowed to instantiate metavariables in the type (see agda#2834)

jespercockx added a commit to jespercockx/agda that referenced this issue Dec 18, 2017

jespercockx added a commit to jespercockx/agda that referenced this issue Jan 5, 2018

[ new ] Big refactoring of the LHS checker
This (partially) reimplements the algorithm for checking left-hand sides.

- In patterns, dot pattern instantiations, absurd patterns, as patterns, etc. are treated uniformly as "problem equations" between an abstract pattern and an internal term.
- Internal patterns now carry "pattern origin" tags to remember what pattern was originally written by the user. This gives a much more robust way to print patterns as the user wrote them.
- The new implementation is much more flexible with regards to the placement of dot patterns. In particular, variables never require a dot anymore (see test/Succeed/Issue473-1606.agda).
- Case splitting is no longer allowed to instantiate metavariables in the type (see agda#2834)

jespercockx added a commit to jespercockx/agda that referenced this issue Jan 5, 2018

jespercockx added a commit to jespercockx/agda that referenced this issue Jan 15, 2018

[ new ] Big refactoring of the LHS checker
This (partially) reimplements the algorithm for checking left-hand sides.

- In patterns, dot pattern instantiations, absurd patterns, as patterns, etc. are treated uniformly as "problem equations" between an abstract pattern and an internal term.
- Internal patterns now carry "pattern origin" tags to remember what pattern was originally written by the user. This gives a much more robust way to print patterns as the user wrote them.
- The new implementation is much more flexible with regards to the placement of dot patterns. In particular, variables never require a dot anymore (see test/Succeed/Issue473-1606.agda).
- Case splitting is no longer allowed to instantiate metavariables in the type (see agda#2834)

jespercockx added a commit that referenced this issue Jan 16, 2018

[ new ] Big refactoring of the LHS checker
This (partially) reimplements the algorithm for checking left-hand sides.

- In patterns, dot pattern instantiations, absurd patterns, as patterns, etc. are treated uniformly as "problem equations" between an abstract pattern and an internal term.
- Internal patterns now carry "pattern origin" tags to remember what pattern was originally written by the user. This gives a much more robust way to print patterns as the user wrote them.
- The new implementation is much more flexible with regards to the placement of dot patterns. In particular, variables never require a dot anymore (see test/Succeed/Issue473-1606.agda).
- Case splitting is no longer allowed to instantiate metavariables in the type (see #2834)

jespercockx added a commit that referenced this issue Jan 16, 2018

@jespercockx jespercockx moved this from Issues to Fixed issues in Merge LHS and coverage checking Feb 17, 2018

@asr asr added this to the 2.5.4 milestone May 25, 2018

@asr asr added the language-change label May 28, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment