[GHC] #13105: Allow type families in RuntimeReps

#13105: Allow type families in RuntimeReps -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 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: -------------------------------------+------------------------------------- Conal Elliott provided me with this puzzle: {{{ type family RepRep a ∷ RuntimeRep class HasRep a where type Rep a ∷ TYPE (RepRep a) repr ∷ a → Rep a abst ∷ Rep a → a type instance RepRep Int = IntRep instance HasRep Int where type Rep Int = Int# abst n = I# n repr (I# n) = n }}} I think we should accept. However, doing so (even with my solution to #12809 complete) is hard, because we frequently consult a kind in order to determine a runtime representation. When that kind is `TYPE (RepRep Int)`, the code generator throws up its arms in despair. The solution here is either to teach the code generator how to normalise types (requiring propagating the `FamInstEnvs`) or to do a whole-program transformation at some point (zonker? desugarer? maybe we can wait until !CorePrep or even unarisation?) to change ids whose types have kinds like `TYPE (RepRep Int)` into ids with types with kinds like `TYPE IntRep`. But I don't want to let this hold me up at the moment, so I'm posting here as a reminder to revisit this problem. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13105 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13105: Allow type families in RuntimeReps -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T13105 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * testcase: => typecheck/should_fail/T13105 Comment: I've added a test case (in my work on #12809, at Phab:D2842), but it's a `compile_fail` test, just because code like this originally made my branch panic. It doesn't panic now, and I want to keep it that way until this bug is addressed properly. Fixing this bug should make the test succeed. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13105#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13105: Allow type families in RuntimeReps -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T13105 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * keywords: => LevityPolymorphism -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13105#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13105: Allow type families in RuntimeReps -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T13105 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
When that kind is TYPE (RepRep Int), the code generator throws up its arms in despair.
So presumably the Lint check that every argument is not levity-polymorphic fails? Actually seeing the code fragment would be helpful. Assuming it's a Lint failure (which I think it could be), can't the type checker just normalise before spitting out the argument code? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13105#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13105: Allow type families in RuntimeReps -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T13105 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Yes, the levity-polymorphism check sees the problem and reports a type of kind `TYPE (RepRep Int)` as levity-polymorphic. I will have a note in the manual about this. If the type checker didn't catch it, it would be a lint error, yes. I don't think it's as simple as a normalisation step in the type checker. For example: {{{ foo :: forall (a :: TYPE (RepRep Int)). a -> a foo x = x }}} In this code, `x` has type `a`. What's to normalise about that?? Now we could say that `x :: a |> co` where `co :: TYPE (RepRep Int) ~ TYPE IntRep`. But now `x`'s type has changed and that means we need to use casts wherever `x` has been used. And this is an easy case where the type checker can see the correct, normalised type from the get-go. In general, unification and type family reduction may be necessary before we can proceed. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13105#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13105: Allow type families in RuntimeReps -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T13105 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I was thinking of this as an adjunct to the LP test in the desugarer. If the argument of an application has type `ty :: TYPE k`, and `k` does not pass the LP test (yet), then normalise `k` (using top level instances only) and cast the arg wtih a coercion `TYPE k ~ TYPE k_norm`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13105#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13105: Allow type families in RuntimeReps -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T13105 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): But that means the argument would change type from `ty` to `ty |> co`. Other bits of the expression might have to change, too. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13105#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13105: Allow type families in RuntimeReps -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T13105 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Sure. Instead of `f e` we'd have `f (e |> co)`. That's fine. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13105#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13105: Allow type families in RuntimeReps -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T13105 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): But if `f e` is well-typed, then `f (e |> co)` surely isn't. We would need `(f |> co') (e |> co)` or some such. I imagine this is what we'll have to do, but it doesn't seem trivial. The other possibility may be to normalise types as we're converting to Stg, where types don't matter. This poses other challenges, in that the levity-polymorphism checks in the desugarer and in Core Lint will have to distinguish between type family applications that can reduce and those that can't. Might be easier than the program transformation, though. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13105#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13105: Allow type families in RuntimeReps
-------------------------------------+-------------------------------------
Reporter: goldfire | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.0.1
Resolution: | Keywords:
| LevityPolymorphism
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
| typecheck/should_fail/T13105
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg

#13105: Allow type families in RuntimeReps -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T13105 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): NB: The above commit does ''not'' fix this! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13105#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13105: Allow type families in RuntimeReps -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T13105 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by magesh.b): * cc: magesh.b (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13105#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13105: Allow type families in RuntimeReps -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T13105 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by magesh.b): {{{#!haskell class Unbox (t :: *) (r :: TYPE k) | t -> r, r -> t where unbox :: t -> r box :: r -> t instance Unbox Int Int# where unbox (I# i) = i box i = I# i instance Unbox Char Char# where unbox (C# c) = c box c = C# c instance (Unbox a a', Unbox b b') => Unbox (a,b) (# a', b' #) where unbox (a,b) = (# unbox a, unbox b #) box (# a, b #) = (box a, box b) -- Works fine testInt :: Int testInt = box (unbox 1) -- Throws an error at call site {-error: • Couldn't match a lifted type with an unlifted type When matching the kind of ‘Int#’ • In the expression: box (unbox (1, 'a')) In an equation for ‘testTup’: testTup = box (unbox (1, 'a')) | 168 | testTup = box (unbox (1, 'a')) | ^^^^^^^^^^^^^^^^^^^^ -} testTup :: (Int, Char) testTup = box (unbox (1, 'a')) }}} Does this error related to same bug? Any chance of such code to work in future GHC release or is it fundamentally not possible to have a levity polymorphic class as a constraint in an instance declaration. One of the use case is, above code would have allowed me to pack user defined data type in to highly packed unboxed anonymous record (using nested Unboxed Tuple) making boxing/unboxing first class in GHC. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13105#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13105: Allow type families in RuntimeReps -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T13105 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by vagarenko): * cc: vagarenko (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13105#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13105: Allow type families in RuntimeReps -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T13105 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): comment:12 seems unrelated, but is problematic. See #14185. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13105#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC