[GHC] #11736: Allow unsaturated uses of unlifted types in Core

#11736: Allow unsaturated uses of unlifted types in Core -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: feature | Status: new request | Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Currently Core Lint checks for unsaturated uses of unlifted types in . These are easily produced in the new type-indexed `Typeable` scheme. For instance, consider solving for `Typeable # (Array# Int)`: * We decompose the application into wanteds `Typeable (* -> #) Array#` and `Typeable * Int` * We construct dictionaries for both, giving us a term `typeRepArray# :: TypeRep (* -> #) Array#` While nothing seems to blow up with this patch, {{{#!patch diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs index 99625c9..2c401de 100644 --- a/compiler/coreSyn/CoreLint.hs +++ b/compiler/coreSyn/CoreLint.hs @@ -1040,7 +1040,7 @@ lintType ty@(TyConApp tc tys) = lintType ty' -- Expand type synonyms, so that we do not bogusly complain -- about un-saturated type synonyms - | isUnliftedTyCon tc || isTypeSynonymTyCon tc || isTypeFamilyTyCon tc + | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc -- Also type synonyms and type families , length tys < tyConArity tc = failWithL (hang (text "Un-saturated type application") 2 (ppr ty)) }}} I otherwise have no reason to believe that this is safe. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11736 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11736: Allow unsaturated uses of unlifted types in Core -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I believe this is OK. But we're beyond the scope of any proof I'm aware of for safety -- none have considered unlifted types, to my knowledge. Simon? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11736#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11736: Allow unsaturated uses of unlifted types in Core -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * cc: sweirich@…, dimitris (added) Comment: The issue with un-saturated type function is to do with abstraction. What if you had {{{ (/\(a:: * -> *). blah) F }}} where `F` is a type function. Well bad things, if you can decompose applications of `a` in `blah`. I think that's the only thing that can go wrong with un-saturated unlifted type constructors. What if we said {{{ (/\(a :: * -> *). blah) Array# }}} Would that be OK? Well, no: `Array# Int` is an unlifted type, not `*`. So it's ill-kinded. But I think this would be fine {{{ (/\(a :: TYPE 'PtrRepLifted -> TYPE 'PtrRepUnlifted). blah) Array# }}} Inside `blah` a variable `x :: a Int` would be an unlifted type, evaluated call-by-value, just as it should. Moreover stranger things like {{{ (/\(a :: Type 'PtrRepLifted -> TYPE 'VoidRep). blah) State# }}} Now inside blah a variable `x :: a Int` would be an unboxed zero-width void thing. Just right. In short I think this is absolutely fine. We don't even need to do anything! (I vote for the above patch.) All we need is someone to come up with a proper account of runtime-rep polymorphism. Kenny? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11736#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11736: Allow unsaturated uses of unlifted types in Core -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): See also #11722 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11736#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11736: Allow unsaturated uses of unlifted types in Core -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): What about unboxed tuples? Right now, we have, e.g., `(# , #) :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep). TYPE r1 -> TYPE r2 -> TYPE 'UnboxedTupleRep`. Of course, `UnboxedTupleRep` is a lie, because unboxed tuples have all sorts of representations. There is an explicit check for this along with the check for runtime representation polymorphism. With those checks in place, what can go wrong even if we unsaturate unboxed tuples? I think it's OK. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11736#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11736: Allow unsaturated uses of unlifted types in Core -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Oh bother, yes, you are right about unboxed tuples. What do you mean about "there is an explicit check for this"? You mean: we allow unrestricted un-saturated primitive type constructors, but enforce some other invariant? There really is a paper here somewhere. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11736#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11736: Allow unsaturated uses of unlifted types in Core -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): See `Note [Unboxed tuples in representation polymorphism check]` in !TcHsSyn. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11736#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11736: Allow unsaturated uses of unlifted types in Core -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => Typeable -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11736#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11736: Allow unsaturated uses of unlifted types in Core -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Typeable, | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: Typeable => Typeable, LevityPolymorphism -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11736#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11736: Allow unsaturated uses of unlifted types in Core -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Typeable, | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * owner: => goldfire Comment: Richard, what is the current status of this? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11736#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11736: Allow unsaturated uses of unlifted types in Core -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Typeable, | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Phab:D2842 will make this possible. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11736#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11736: Allow unsaturated uses of unlifted types in Core
-------------------------------------+-------------------------------------
Reporter: bgamari | Owner: goldfire
Type: feature request | Status: new
Priority: normal | Milestone: 8.2.1
Component: Compiler | Version: 8.1
Resolution: | Keywords: Typeable,
| LevityPolymorphism
Operating System: Unknown/Multiple | Architecture:
Type of failure: GHC rejects | Unknown/Multiple
valid program | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg

#11736: Allow unsaturated uses of unlifted types in Core -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: feature request | Status: closed Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: fixed | Keywords: Typeable, | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T11736 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * testcase: => typecheck/should_compile/T11736 * status: new => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11736#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC