[Agda-dev] Missing required `Eq Expr` constraint?

[Andrés Sicard-Ramírez]

Hi,

In the *maint.2.4.2* branch, with exception of the instance

  instance Underscore Expr where    (*)
  ...

defined in the module Syntax.Abstract, all the instances of the type
class

  class Eq a => Underscore a where
  ...

defined in the module Syntax.Common, satisfy the constraint `Eq a`.

Why the instance (*) is type-checked?

Best,


-- 
Andrés