[Agda] Incompatibilities affecting ``Fresh Look''

[Julian Beaumont]

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.)
>
>
> Wolfram

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.