[Agda] Incompatibilities affecting ``Fresh Look''

[Julian Beaumont]

On Thu, Dec 16, 2010 at 12:10 AM, <kahl at cas.mcmaster.ca> wrote:
>
> > On Wed, Dec 15, 2010 at 1:31 PM, <kahl at cas.mcmaster.ca> wrote:
> > >
> > > I am therefore adding the old definition to their Data.Maybe.Extras;
> > > this also involves the following lib-0.3 function:
> > >
> > >  drop-just : ∀ {A : Set} {x y : A} → just x ≡ just y → x ≡ y
> > >  drop-just refl = refl
> > >
> > > I tried to adapt this to:
> > >
> > >  drop-just′ : {a : Level} {A : Set a} {x y : A} → just x ≡ just y → x ≡ y
> > >  drop-just′ {a} {A} {x} {y} refl = refl {x} {y}
> > >
> > > /var/tmp/AGDA/pouillard-pottier-fresh-look-agda-2010/Data/Maybe/Extras.agda:32,28-32
> > > Failed to solve the following constraints:
> > >  _59 == _60 : _58
> > > when checking that the pattern refl has type _59 ≡ _60
> > >
> > > If I postulate drop-just′, it's usage in decPESetoid and the usage of that
> > > in NotSoFresh.Derived go through.
> > >
> > > Why did this work before and does not work now?
> > > For proj₁-injective, I know that the treatment of records
> > > has changed, but here, I don't know which of the changes in the past
> > > year might affect this definition.
> > > (I would not expect that universe-polymorphism is to blame.)
>
> Dan Licata <drl at cs.cmu.edu> proposed using a dot pattern,
> which by itself does not help:
>
>  drop-just′ : {a : Level} {A : Set a} {x y : A} → just x ≡ just y → x ≡ y
>  drop-just′ {a} {A} {x} {.x} refl = refl
>
> /var/tmp/AGDA/pouillard-pottier-fresh-look-agda-2010/Data/Maybe/Extras.agda:32,29-33
> Failed to solve the following constraints:
>  _59 == _60 : _58
> when checking that the pattern refl has type _59 ≡ _60
>
>
>
> On Wed, Dec 15, 2010 at 03:17:36PM +1000, Julian Beaumont wrote:
> > It looks like the addition of universe polymorphism causes agda to
> > fail to infer some of the implicit arguments in the first use of _≡_.
> > Changing it to:
> >
> > drop-just′ : {a : Level} {A : Set a} {x y : A} → _≡_ {a} {Maybe A}
> > (just x) (just y) → x ≡ y
> > drop-just′ refl = refl
> >
> > seems to work.
>
> It does, thank you!
>
>
>
> The following three work, too:
>
>  drop-just′ : {a : Level} {A : Set a} {x y : A} → _≡_ {_} {Maybe A} (just x) (just y) → x ≡ y
>  drop-just′ refl = refl
>
>  drop-just′ : {a : Level} {A : Set a} {x y : A} → _≡_ {_} {Maybe _} (just x) (just y) → x ≡ y
>  drop-just′ refl = refl
>
>  drop-just′ : {a : Level} {A : Set a} {x y : A} → _≡_ {_} {Maybe {_} _} (just x) (just y) → x ≡ y
>  drop-just′ refl = refl
>
> However, taking out the Maybe, too, fails
> (as expected, since we are back to original with that):
>
>  drop-just′ : {a : Level} {A : Set a} {x y : A} → _≡_ {_} {_} (just x) (just y) → x ≡ y
>  drop-just′ refl = refl
>
> Failed to solve the following constraints:
>  _59 == _60 : _58
> when checking that the pattern refl has type _59 ≡ _60
>
>
> I do not understand how Maybe cannot be inferred from ``just x ≡ just y'';
> after all, we are just dealing with the following two definitions here:
>
>
> data Maybe {a} (A : Set a) : Set a where
>  just    : (x : A) → Maybe A
>  nothing : Maybe A
>
> data _≡_ {a} {A : Set a} (x : A) : A → Set a where
>  refl : x ≡ x
>
>
> So why does the Maybe not propagate from the just to the _≡_ in ``just x ≡ just y''?
>
>
> Wolfram

Looking at this a little more the following also works:

just′ : {a : Level} {A : Set a} → A → Maybe A
just′ x = just x

drop-just′ : {a : Level} {A : Set a} {x y : A} → just′ x ≡ just′ y → x ≡ y
drop-just′ refl = refl

I believe this issue is a result of constructors being overloaded. In
particular, agda allowing multiple constructors to have the same name
and selects the appropriate one for each use site based on the type of
the result. This prevents agda from deducing the type of "just x"
since it needs to know [part of] the type of "just x" before it can
decide which constructor just refers to. Presumably in this case
there's only one definition of just in scope and so the compiler
should be able to select it even without knowing the expected type but
it doesn't appear to do this at the moment.

In the annotated versions the expected type is known to be "Maybe ?"
which is enough information for agda to decide which constructor is
meant by "just x". The version with the just′ function works because
functions can't be overloaded in the same way constructors can.