[GHC] #13262: Allow type synonym family application in instance head if it reduces away
#13262: Allow type synonym family application in instance head if it reduces away -------------------------------------+------------------------------------- Reporter: ezyang | Owner: Type: feature | Status: new request | Priority: lowest | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- GHC rejects the following program: {{{ {-# LANGUAGE TypeFamilies, FlexibleInstances #-} module F where type family F a type instance F Int = Int -> Int instance Show (F Int) where show _ = "fun" }}} But this doesn't seem fundamentally problematic to me: at the instance declaration, we know that F Int will reduce, and after that reduction there isn't any problem with the instance. Here's a less restrictive instance head test: first, we reduce type families as much as possible. Then, if there are still leftover non- reducing type families, reject the instance. After having typed this up, I have realized that I don't actually need this feature. But I'm filing it here for posterity. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13262 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13262: Allow type synonym family application in instance head if it reduces away -------------------------------------+------------------------------------- Reporter: ezyang | Owner: Type: feature request | Status: new Priority: lowest | 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: | -------------------------------------+------------------------------------- Comment (by rwbarton): Perhaps we should guard the "first, we reduce type families as much as possible" step with the `TypeSynonymInstances` extension (which is implied by `FlexibleInstances`, apparently). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13262#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13262: Allow type synonym family application in instance head if it reduces away -------------------------------------+------------------------------------- Reporter: ezyang | Owner: Type: feature request | Status: new Priority: lowest | 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: | -------------------------------------+------------------------------------- Comment (by goldfire): This has been proposed before (though I can't find where), and I find the idea quite distasteful. Consider what this would mean at the term level: {{{ f :: Bool -> Int f (not True) = 5 f True = 6 }}} Parsing challenges aside, there's nothing at all wrong with the above declaration. But do we really want programmers to be able to do this? It's the same at the type level. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13262#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13262: Allow type synonym family application in instance head if it reduces away -------------------------------------+------------------------------------- Reporter: ezyang | Owner: Type: feature request | Status: new Priority: lowest | 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: | -------------------------------------+------------------------------------- Comment (by ezyang): By analogy, though, `TypeSynonymInstances` are also distasteful, because it's effectively letting you write `myfalse = False; f myfalse = 5` (well, that doesn't actually do what you want in Haskell today :o) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13262#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13262: Allow type synonym family application in instance head if it reduces away -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: feature request | Status: new Priority: lowest | 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: | -------------------------------------+------------------------------------- Comment (by goldfire): Agreed. But vanilla type synonyms are much simpler than type families. It's all a judgment call. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13262#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#13262: Allow type synonym family application in instance head if it has no free variables -------------------------------------+------------------------------------- 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: 12680 Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13262#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13262: Allow type synonym family application in instance head if it has no free variables -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 12680 Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by ezyang): * keywords: => backpack -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13262#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13262: Allow type synonym family application in instance head if it has no free variables -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 12680 Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by ezyang): This seems to be more complicated than just lifting the restriction, because whenever we have a wanted Show (F T) (where F is the type family), we always flatten this into Show a, a ~ F T; and of course, there is never an instance of Show for a in the top-level. I'm not entirely sure how the solver solves this when Show (F T) is a local constraint; some guidance here would be appreciated. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13262#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13262: Allow type synonym family application in instance head if it has no free variables -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 12680 Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Let's not do this unless there is a really compelling reason. More complication. And soon you'll want {{{ type instance F (G [a]) = blah }}} to work, assuming that `G [a]` can reduce to (say) `[Tree a]`. This way lies madness. Let's not complicate the language of type patterns. Yet anyway. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13262#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13262: Allow type synonym family application in instance head if it has no free variables -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 12680 Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by ezyang): Oh all right. We can wait till someone else pipes in and requests this :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13262#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13262: Allow type synonym family application in instance head if it has no free variables -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 12680 Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Artyom.Kazak): * cc: Artyom.Kazak (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13262#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13262: Allow type synonym family application in instance head if it has no free variables -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 12680 Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Artyom.Kazak):
Oh all right. We can wait till someone else pipes in and requests this :)
That would be me! My usecase is generating anonymous records and then defining SafeCopy migrations for them (see http://hackage.haskell.org/package/safecopy-0.9.4.1/docs/Data- SafeCopy.html#t:Migrate). Essentially this: {{{ type Foo_v1 = ... type Foo_v2 = AddField "name" Text Foo_v1 type Foo_v3 = RemoveField "age" Foo_v2 }}} All of that is implemented via type families. The problem is that now I can't have instances for these types (e.g. `instance Migrate Foo_v3`). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13262#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13262: Allow type synonym family application in instance head if it has no free variables -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 12680 Related Tickets: 13773 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Artyom.Kazak): * related: => 13773 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13262#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13262: Allow type synonym family application in instance head if it has no free variables -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 12680 Related Tickets: #13773 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Artyom.Kazak): * related: 13773 => #13773 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13262#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC