[GHC] #1207: Unnecessary prohibition of unquantified higher-order typeclass constraints

GHC trac at galois.com
Wed Mar 7 09:51:44 EST 2007


#1207: Unnecessary prohibition of unquantified higher-order typeclass constraints
----------------------------------------+-----------------------------------
    Reporter:  br276 at cam.ac.uk          |       Owner:          
        Type:  bug                      |      Status:  new     
    Priority:  low                      |   Milestone:          
   Component:  Compiler (Type checker)  |     Version:  6.6     
    Severity:  minor                    |    Keywords:          
  Difficulty:  Unknown                  |    Testcase:          
Architecture:  Multiple                 |          Os:  Multiple
----------------------------------------+-----------------------------------
In GHC 6.6, attempting to declare a function (say f) with a type of the
 form
 {{{
 forall t. ... -> (Num t => ...) -> ...
 }}}
 produces the error:
 {{{
 All of the type variables in the constraint `Num t' are already in scope
     (at least one must be universally quantified here)
 }}}
 This used to make sense -- after all, there's no way f can deduce a Num
 constraint on t that wasn't provided by its caller, so a higher-order
 argument with this sort of type is uncallable. But with the addition of
 GADTs, this is no longer true, since another of f's arguments might, when
 deconstructed, reveal that t is in fact an Int or a Ratio u. In fact, GADT
 deconstructors can have types like this. E.g.
 {{{
 data Foo a where
   Bar :: forall a. Num a => a -> Foo a
 }}}
 has a deconstructor of type
 {{{
 forall a r. Foo a -> (Num a => a -> r) -> r
 }}}
 So I think that these types should be allowed, although I haven't found a
 use for them yet except for writing GADT deconstructors.

 On the other hand, one can't write deconstructors for most GADTs even with
 this change, so perhaps it's the wrong change. If explicit type equality
 constraints were allowed in Haskell, then I could write
 {{{
 forall t. ... -> (forall t'. (t ~ t', Num t') => ...) -> ...
 }}}
 instead.

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/1207>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler


More information about the Glasgow-haskell-bugs mailing list