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

[Andrés Sicard-Ramírez]

On 17 November 2015 at 06:33, Andrés Sicard-Ramírez <asr at eafit.edu.co> wrote:
> 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?

Self answer:

Because in Syntax.Abstract we have

  type Color = Expr

  instance Eq Color where
  ...

(Sorry for the noise)

Best,

-- 
Andrés