[Haskell-cafe] Re: checking types with type families

[Dan Doel]

On Friday 02 July 2010 6:23:53 pm Claus Reinke wrote:
> -- second, while trying the piece with classic, non-equality constraints
> Prelude> (id :: (forall b. Eq b=>b->b) -> (forall b. Eq b=>b->b))
> 
> <interactive>:1:0:
>     No instance for (Show ((forall b1. (Eq b1) => b1 -> b1) -> b -> b))
>       arising from a use of `print' at <interactive>:1:0-55
>     Possible fix:
>       add an instance declaration for
>       (Show ((forall b1. (Eq b1) => b1 -> b1) -> b -> b))
>     In a stmt of an interactive GHCi command: print it
> 
> Note that the second version goes beyond the initial problem,
> to the missing Show instance, but the error message loses the
> Eq constraint on b!
> 
> -- it is just the error message, the type is still complete
> Prelude> :t (id :: (forall b. Eq b=>b->b) -> (forall b. Eq b=>b->b))
> (id :: (forall b. Eq b=>b->b) -> (forall b. Eq b=>b->b))
> 
>   :: (Eq b) => (forall b1. (Eq b1) => b1 -> b1) -> b -> b
> 
> I don't have a GHC head at hand, perhaps that is doing better?

I don't think this is a big deal. For instance:

  Prelude> :t id :: Eq b => b -> b
  id :: Eq b => b -> b :: (Eq b) => b -> b
  Prelude> id :: Eq b => b -> b

  <interactive>:1:0:
      No instance for (Show (b -> b))
        arising from a use of `print' at <interactive>:1:0-19
      Possible fix: add an instance declaration for (Show (b -> b))
      In a stmt of a 'do' expression: print it

The Eq constraint is irrelevant to the fact that there is no b -> b Show 
instance. The search for an instance looks only at the type part, and if it 
finds a suitable match, then checks if the necessary constraints are also in 
place.

What's happening in your example is that the type:

  (forall b. Eq b => b -> b) -> (forall b. Eq b => b -> b)

is being changed to the isomorphic type:

  forall b. Eq b => (forall b. Eq b => b -> b) -> b -> b

And then the instance search only looks at the part after the first =>, which 
fails to match any Show instances.

-- Dan