[Agda] Incompatibilities affecting ``Fresh Look''

[Nils Anders Danielsson]

On 2010-12-15 17:28, Julian Beaumont wrote:
> 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.

data Eq {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) : Rel (Maybe A) (a ⊔ ℓ) where
   just    : ∀ {x y} (x≈y : x ≈ y) → Eq _≈_ (just x) (just y)
   nothing : Eq _≈_ nothing nothing

-- 
/NAD