[Agda] Incompatibilities affecting ``Fresh Look''

[kahl at cas.mcmaster.ca]

> 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