haskell-cafe@haskell.org
[Top] [All Lists]

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

Subject: Re: [Haskell-cafe] Re: checking types with type families
From: "Claus Reinke"
Date: Sat, 3 Jul 2010 00:23:53 +0200
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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@xxxxxxxxxxx
http://www.haskell.org/mailman/listinfo/haskell-cafe

<Prev in Thread] Current Thread [Next in Thread>