| data T = Foo (forall a. Enum a => (a->a)) | | could indeed be local universal quantification. You can construct a | Foo with any function of type (Enum=>a->a), e.g. (Foo succ) is ok, | (Foo id) is not. When you pattern-match on the constructor, you get | back the original universal type, e.g. the following is valid: | | f :: T -> (Int,Bool,Char) | f (Foo g) = (g 0, g False, g 'a') | | It appears that ghc, Hugs, and nhc98 do not support local universals, | although hbc does. GHC and Hugs both do. In fact, GHC supports arbitrary-rank universal quantification. Simon
"Simon Peyton-Jones"
GHC and Hugs both do. In fact, GHC supports arbitrary-rank universal quantification.
The example I tried failed, so I assumed it wasn't supported. $ cat Exists.hs module Exists where data T = forall a. Enum a => Foo (a->a) f :: T -> (Int,Bool,Char) f (Foo g) = (g 0, g False, g 'a') $ ghc -fglasgow-exts -c Exists.hs Exists.hs:4: Couldn't match `Int' against `Bool' Expected type: Int Inferred type: Bool In the first argument of `g', namely `False' In the definition of `f': (g 0, g False, g 'a') Regards, Malcolm
participants (2)
-
Malcolm Wallace -
Simon Peyton-Jones