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

[Claus Reinke]

> f :: forall a b. C a b => T a -> Bool
> f T1 = True
> f T2 = (op :: a -> b) 3
> 
> as that results in the counter-intuitive
> 
>    Couldn't match expected type `Bool' against inferred type `b'
>      `b' is a rigid type variable bound by
>          the type signature for `f'
>            at C:\Users\claus\Desktop\tmp\fd-local.hs:17:14
>    In the expression: (op :: a -> b) 3
>    In the definition of `f': f T2 = (op :: a -> b) 3
> 
> Which seems to be a variant of Oleg's example? 

If it is, it is a simpler variant, because it has a workaround:

f :: forall a b. C a b => T a -> Bool
f T1 = True
f T2 = (op :: C a b1 => a -> b1) 3

While playing around with Oleg's example, I also found the
following two pieces (still ghc-6.12.3):

-- first, a wonderful error message instead of expected simplification
Prelude> (id :: (forall b. b~Bool=>b->b) -> (forall b. b~Bool=>b->b))

<interactive>:1:1:
    Couldn't match expected type `forall b. (b ~ Bool) => b -> b'
           against inferred type `forall b. (b ~ Bool) => b -> b'
      Expected type: forall b. (b ~ Bool) => b -> b
      Inferred type: forall b. (b ~ Bool) => b -> b
    In the expression:
        (id ::
           (forall b. (b ~ Bool) => b -> b)
           -> (forall b. (b ~ Bool) => b -> b))
    In the definition of `it':
        it = (id ::
                (forall b. (b ~ Bool) => b -> b)
                -> (forall b. (b ~ Bool) => b -> b))

-- 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?

Claus