Why doesn't this typecheck?

Question

This is toy-example.hs:

{-# LANGUAGE ImpredicativeTypes #-}

import Control.Arrow

data From = From (forall a. Arrow a => a Int Char -> a [Int] String)

data Fine = Fine (forall a. Arrow a => a Int Char -> a () String)

data Broken = Broken (Maybe (forall a. Arrow a => a Int Char -> a () String))

fine :: From -> Fine
fine (From f) = Fine g
  where g :: forall a. Arrow a => a Int Char -> a () String
        g x = f x <<< arr (const [1..5])

broken :: From -> Broken
broken (From f) = Broken (Just g) -- line 17
  where g :: forall a. Arrow a => a Int Char -> a () String
        g x = f x <<< arr (const [1..5])

And this is what ghci thinks of it:

GHCi, version 7.0.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Loading package ffi-1.0 ... linking ... done.
Prelude> :l toy-example.hs 
[1 of 1] Compiling Main             ( toy-example.hs, interpreted )

toy-example.hs:17:32:
    Couldn't match expected type `forall (a :: * -> * -> *).
                                  Arrow a =>
                                  a Int Char -> a () String'
                with actual type `a0 Int Char -> a0 () String'
    In the first argument of `Just', namely `g'
    In the first argument of `Broken', namely `(Just g)'
    In the expression: Broken (Just g)
Failed, modules loaded: none.

Why does fine typecheck while broken does not?

How do I get broken to typecheck?

(In my real code I can add the type parameter a to Broken if I have to, instead of having it universally quantified inside the constructor, but I'd like to avoid this if possible.)

---

Edit: If I change the definition of Broken to

data Broken = Broken (forall a. Arrow a => Maybe (a Int Char -> a () String))

then broken typechecks. Yay!

But if I then add the following function

munge :: Broken -> String
munge (Broken Nothing) = "something"  -- line 23
munge (Broken (Just f)) = f chr ()

then I get the error message

toy-example.hs:23:15:
    Ambiguous type variable `a0' in the constraint:
      (Arrow a0) arising from a pattern
    Probable fix: add a type signature that fixes these type variable(s)
    In the pattern: Nothing
    In the pattern: Broken Nothing
    In an equation for `munge': munge (Broken Nothing) = "something"

How do I get munge to typecheck as well?

2nd edit: In my real program I have replaced the Broken (Maybe ...) constructor with BrokenNothing and BrokenJust ... constructors (there were already other constructors), but I'm curious how pattern matching is supposed to work in this situation.

Answer 1

ImpredicativeTypes leaves you on quite shaky ground that changes from GHC version to version in any case - they're struggling to find a formulation of impredicativity that appropriately balances power, ease of use and ease of implementation.

In this particular case, trying to put a quantified type inside a Maybe, which is a datatype not explicitly defined to behave this way, is really tricky, so I'd advise going for the custom-defined constructors instead as you mention.

I think that you can fix munge above by re-deconstructing the argument to Broken on the RHS, at a time when the type its being used as will be known, e.g.:

munge (Broken x@(Just _)) = fromJust x chr ()

It's pretty ugly, though.