[Agda] Agdas constraint solver too eager?!
Andreas Abel
andreas.abel at ifi.lmu.de
Fri Sep 7 15:13:04 CEST 2012
A consequence of making Agda aware of unused arguments is that certain
"phantom-type" tricks do not work anymore.
data D (phantom : Nat) : Set where
c : D phantom
If Agda may recognize 'phantom' as unused, then
D 0 = D 1
and accordingly, D X = D 0 will not solve X to 0. It will be necessary
then to replace D by
data D : Nat -> Set where
c : {phantom : Nat} -> D phantom
to get the desired effect. The same fix however does not work for
records with phantom parameters (since there are no indexed records).
There is a choice to make:
1. Go the 'semantic path' for data type parameters, allowing Agda to
recognize them as unused. That will make certain phantom tricks
impossible.
I am a bit confused, since I thought by getting rid of injective
type constructors we had already gotten there, but it seems not.
2. Go the 'syntactic path' for data type parameters, considering them
never as unused, to allow phantom tricks.
The relationship to injective type constructors should be
clarified then.
I am tending towards 1., but people using phantoms should speak up to
discuss whether they are essential and whether they could sustain when
going 1.
Cheers,
Andreas
On 07.09.2012 12:49, Andreas Abel wrote:
> I would not have expected the following program to type check:
>
> assert : (A : Set) → A → Bool → Bool
> assert _ _ true = true
> assert _ _ false = false
>
> g : Bool -> Bool -> Bool
> g x true = true
> g x false = true
>
> unsolved : Bool -> Bool
> unsolved y =
> let X : Bool
> X = _
> in assert (g X y ≡ g true y) refl X
>
> istrue : (unsolved false) ≡ true
> istrue = refl
>
> The meta-variable X is solved to 'true' (as witnessed by istrue), even
> though 'false' would also be a solution, semantically, because g
> actually ignores its first argument. (It even ignores its second
> argument, but that does not matter here.)
>
> The expected behavior would be an unsolved X, since it is not uniquely
> determined.
>
> I came across this example when working on making Agda aware of unused
> arguments (so as to fix issue 44).
>
> I think we should stick to the philosophy that constraint solving should
> only deliver unique solutions, and fix the issue described above. That
> would lead to some more unsolved metas, I am afraid...
>
> Cheers,
> Andreas
>
--
Andreas Abel <>< Du bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
More information about the Agda
mailing list