[GHC] #15905: Data familes should end in Type
#15905: Data familes should end in Type -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 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: -------------------------------------+------------------------------------- Currently we allow {{{ data family Fix (f :: Type -> k) :: k }}} with a ‘k’ in the right-hand corner. See `Note [Arity of data families]` in `FamInstEnv`. That seems attractive because we can then have {{{ data instance Fix (f :: Type -> Type -> Type) (x :: Type) = MkFix2 (f (Fix f x) x) }}} But what about this? {{{ type family F a type instance F Int = Type -> Type data instance Fix (f :: Type -> F Int) (x :: Type) = … }}} The type inference engine (tcInferApps) will type the LHS as something like {{{ ((Fix (f :: Type -> F Int)) |> co1) (x |> co2) where co1 :: F Int ~ Type co2 :: Type ~ F Int }}} But the LHS of a family axiom has to look like {{{ F t1 t2 … tn }}} not {{{ ((F t1 |> co) t2 t3) |> co4) …tn }}} with casts in the way. So that LHS must be rejected. And it’s very hard to see how to accept the first example while (predictably, comprehensibly) rejecting the second. It’d be something like “the kind that instantiates k must have obvious, visible, arrows”. Ugh! And indeed GHC HEAD does accept the first, but rejects the second with the error message {{{ • Expected kind ‘* -> * -> *’, but ‘f :: Type -> F Int’ has kind ‘* -> F Int’ • In the first argument of ‘Fix’, namely ‘(f :: Type -> F Int)’ In the data instance declaration for ‘Fix’ }}} That's clearly bogus: we've specified that `F Int = Type -> Type`. I'm not even sure precisely how it happens, but it must be fragile: a change in solve order, or more aggressive solving might change the behaviour. I don't see how to solve this. I propose instead to require data family kinds to end in `Type`, not in a type ''variable'' (as we currently allow). I don't know how many people that would affect, but the current state of affairs looks untenable. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15905 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15905: Data familes should end in Type -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14645 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #14645 Comment: #14645 would be nuked out of existence if this were implemented. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15905#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15905: Data familes should end in Type -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14645 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Ha ha! I'm in favour of walking (on solid ground) before we run. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15905#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15905: Data familes should end in Type -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14645 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I don't see any reason to throw the baby out with the bathwater here. It's true that extending this feature to work with type families is difficult, but we can continue the status quo. If we want to make sure that we're order-independent, just look for type families in the instantiated kind. If we spot any, fail. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15905#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15905: Data familes should end in Type -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14645 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): My point is that the status quo is extremely fragile -- it relies crucially on eager unification. It's supposed to be the case that we can defer all unifications to the constraint solver, all all will work. But not so! So now, to give a precise spec, we have to make precise which constraints can be solved eagerly and which can be deferred. I hate that. The baby is mingled with the bathwater -- it's a fluke that it works at all. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15905#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15905: Data familes should end in Type -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14645 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by monoidal): Duplicate of #14420? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15905#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15905: Data familes should end in Type -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14645 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Ah yes. Not quite a duplicate of #14420, but it would nail #14420 inter alia. In particular, the description of #14420 says (a bit impreciseely) "We should require that any instantiation of a data family be to a kind that ends in Type." My proposal in this ticket would make that true automatically, because data family kinds would always end in Type, and hence a fortiori so would their instantiations. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15905#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15905: Data familes should end in Type -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14645 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): iceland_jack: Ryan thinks you use this feature a lot. Is that true? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15905#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15905: Data familes should end in Type -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14645 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I'm not Icelandic, but I can provide one "real-world" use case for this feature from the `singletons` library. It used to be the case that we had about eight or so data types of this shape: {{{#!hs data TyCon1 :: (k1 -> k2) -> (k1 ~> k2) data TyCon2 :: (k1 -> k2 -> k3) -> (k1 ~> k2 ~> k3) data TyCon3 :: (k1 -> k2 -> k3 -> k4) -> (k1 ~> k2 ~> k3 ~> k4) data TyCon4 :: (k1 -> k2 -> k3 -> k4 -> k5) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5) data TyCon5 :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6) data TyCon6 :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7) data TyCon7 :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8) data TyCon8 :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> k9) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8 ~> k9) }}} We arbitrarily capped off the maximum at eight. With the advent of polymorphic data family return kinds, however, we were able to consolidate all of this down into just three things: {{{#!hs data family TyCon :: (k1 -> k2) -> unmatchable_fun type family ApplyTyCon (f :: k1 -> k2) (x :: k1) :: k3 where ApplyTyCon (f :: k1 -> k2 -> k3) x = TyCon (f x) ApplyTyCon f x = f x type instance Apply (TyCon f) x = ApplyTyCon f x }}} Now we don't need to copy-paste `TyCon` multiple times, and better yet, we don't have to arbitrarily set a maximum of eight, since `ApplyTyCon` lets us go to whatever arity we desire. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15905#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15905: Data familes should end in Type -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14645 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Some thoughts from this morning's call: * The error report in the original report is unrelated to this ticket: it's just #12088 again. Adding a TH splice does the trick, giving this minimal example: {{{#!hs {-# LANGUAGE PolyKinds, TypeFamilies, DataKinds, TemplateHaskell #-} module Bug where import Data.Kind data family Fix (f :: Type -> k) :: k type family F a type instance F Int = Type -> Type $(return []) data instance Fix (f :: Type -> F Int) (x :: Type) = Mk }}} This is accepted, by transforming the instance to {{{#!hs data instance Fix @(Type -> Type) (f :: Type -> Type) (x :: Type) = Mk }}} In other words, GHC just realizes it can replace `F Int` with `Type -> Type` and carry on. * In an attempt to stop GHC from being this clever, we tried using visible dependent quantification: {{{#!hs data family Fix k (f :: Type -> k) :: k data instance Fix (F Int) (f :: Type -> F Int) (x :: Type) = Mk }}} Note that `k` is explicit now. This panics, because the `unravelFamInstPats` chokes on the strange instance, causing downstream chaos. (Really, `unravelFamInstPats` should panic.) However, if somehow the plumbing were fixed, this would be rejected because it mentions a type family in a type pattern. * In another attempt to defeat the ever-clever GHC, I tried using an explicit forall. {{{#!hs data family Fix (f :: Type -> k) :: k data instance forall (f :: Type -> F Int) (x :: Type). Fix f x = Mk }}} This works by instantiating `Fix` with `Type -> Type` (as before) and casting `f`. * Previously, Simon was worried about the fact that there might be a difference in behavior between eager unification and the work the solver does. But I don't think there is, as `solveEqualities` is called ''before'' `unravelFamInstPats`. * The problem here is really all about when type families get in the way of exposing arrows in the data family's kind. In the `Fix` example, the type family `F Int` obscures the underlying type `Type -> Type`. How do we specify when such a problem exists? * I conjecture that the problem never exists on its own. This obfuscation can happen only in two ways: (1) either some kind parameter has been instantiated with a type family application, or (2) a type family application appears in the return kind of a data family. In case (1), we're blocked by #12564; that case cannot happen. In case (2), we're blocked by #14645. So I think that this ticket, by itself, is redundant currently. If either of those other tickets is fixed, it won't be. * Fixing #12564 is likely to require generalizing (or otherwise changing) the form of type family LHSs, thus fixing this ticket inter alia. So, the upshot is: let's fix #12564 before #14645, and this ticket never needs to be considered again. :) I'm commenting on those two tickets, too. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15905#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15905: Data familes should end in Type -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14645 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
Really, unravelFamInstPats should panic
I agree. Might you find a moment to make it so? Esp now we have a concrete case where chaos happens if we don't. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15905#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15905: Data familes should end in Type -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14645 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => TypeFamilies -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15905#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC