#9568: Type classes that fully cover closed kinds -------------------------------------+------------------------------------- Reporter: dmcclean | Owner: Type: feature | Status: new request | Milestone: ⊥ Priority: lowest | Version: 7.8.3 Component: Compiler | Keywords: (Type checker) | Architecture: Unknown/Multiple Resolution: | Difficulty: Unknown Operating System: | Blocked By: Unknown/Multiple | Related Tickets: Type of failure: | None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by rwbarton): This is a natural thing to want but, alas, it's not so simple. It's not enough for the compiler to know that some instance exists. It has to know which instance to use, because the choice of instance affects the runtime semantics of the program. From a theory point of view, polymorphism over closed kinds has the same parametricity properties as polymorphism over open kinds like `*`. If I have a function `f :: forall (b :: Bool). Proxy b -> String` then `f`'s behavior cannot depend on the choice of `b`, so `f (Proxy :: Proxy False)` must be equal to `f (Proxy :: Proxy True)`, just like a function `g :: Maybe a -> String` must satisfy `g (Nothing :: Maybe Int)` = `g (Nothing :: Maybe Bool)`. From an implementation point of view there is no difference at all at runtime between `Proxy :: Proxy False` and `Proxy :: Proxy True`, so simply for that reason it's impossible for any function to distinguish them. But with a class constraint `C b`, even when `C` has instances for both `False` and `True`, `f`'s behavior can depend on `b`, as I'm sure you know. This is possible because the `C b` constraint gets translated to an extra value-level argument to the function. So, `f :: forall (b :: Bool). C b => Proxy b -> String` is really different from `f :: forall (b :: Bool). Proxy b -> String` even when `C b` is satisfied for each individual type `b :: Bool`. In light of all this, I'm not sure what change along the lines of your suggestion would be possible. IIRC Richard Eisenberg's "dependent Haskell" project includes a non-parametric universal quantifier; perhaps that is related. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9568#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler