On Fri, Jun 19, 2015 at 2:38 PM, Ivan Lazar Miljenovic wrote:

On 19 June 2015 at 22:09, Leza Morais Lutonda wrote:
> On 06/19/2015 03:02 AM, MigMit wrote:
>>
>> Typo.
>>
>> {-# LANGUAGE ConstraintKinds, GADTs #-}
>> data SC c e where SC :: c d => d -> e -> SC c e
>
>
> Yes, I have activated the GADTs extension too and the data definition itself
> typechecks but the Show instance do not:
>
> instance Show e => Show (S c e) where
> show (SC x y) = show x ⧺ show y
>
> Because: Could not deduce (Show d) arising from a use of ‘show’

This works for me if I also enable FlexibleInstances and restrict it to:

instance (Show e) => Show (S Show e) where ...

Note this won't work for a Num instance mentioned earlier because the existentially quantified d types in two SC values are not provably the same type. In other words, you can't write

instance Num e => Show (S Num e) where

SC x1 y1 + SC x2 y2 = SC (x1 + x2) (y1 + y2)

because x1 and x2 can have different types.

Regards,

Sean