#13262: Allow type synonym family application in instance head if it reduces away -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by ezyang): * priority: lowest => low Comment: Actually, I realized that something stronger would be OK here: it's OK for a type family synonym to occur in an instance, even if it doesn't reduce away, AS LONG AS the expression has no free variables. This is pretty useless for normal programmers but actually it is pretty useful in Backpack. Consider: {{{ -- there's some type family F a :: * -> * data T instance Monad (F T) where ... }}} This is something that I'd really quite like to write in a signature, because what I am saying is that there is some existing type family F, and whatever it is the abstract type you picked, F T better reduce to a monad. Yes I could replace the type family with another abstract type for the monad, but if I want Backpack and the type family to coexist, I get better backwards compatibility by reusing the type family. The analogy is how we handle type families in constraints: {{{ f :: Monad (F a) => .... }}} This is OK because `a` is a skolem variable, so we aren't ever going to instantiate it to some variable while we're typechecking the body of f. What would be wrong, and is impossible to write in Haskell's type language today, is `f :: (forall a. Monad (F a)) => ...`! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13262#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler