GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20200924T22:37:40Zhttps://gitlab.haskell.org/ghc/ghc//issues/18624Core Lint error with sneaky use of levity polymorphism in kinds20200924T22:37:40ZRyan ScottCore Lint error with sneaky use of levity polymorphism in kinds#14180 says that levity polymorphism in kinds isn't possible right now. Actually, this is only half true: it's possible if you leverage a backdoor. This backdoor is known as type synonyms:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE UnboxedTuples #}
{# OPTIONS_GHC dcorelint #}
module Bug where
import Data.Kind
type UT = (##) > Type
data S :: UT where
MkS :: S '(##)
```
This program, when compiled with GHC 8.0 or later, will produce a Core Lint error. Here is the error on 8.10.2:
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs dnotypeablebinds
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of CorePrep ***
Bug.hs:12:3: warning:
Kind application error in type ‘a_au1 ~# '()’
Function kind = forall k0 k1. k0 > k1 > TYPE ('TupleRep '[])
Arg kinds = [((# #), TYPE ('TupleRep '[])),
((# #), TYPE ('TupleRep '[])), (a_au1, (# #)), ('(), (# #))]
Forall: k0_10
*
((# #), TYPE ('TupleRep '[]))
In the type of a binder: MkS
In the type ‘forall (a :: (# #)). (a ~# '()) > S a’
Substitution: [TCvSubst
In scope: InScope {a_au1 $WMkS}
Type env: []
Co env: []]
Bug.hs:12:3: warning:
Kind application error in type ‘a_au1 ~# '()’
Function kind = forall k0 k1. k0 > k1 > TYPE ('TupleRep '[])
Arg kinds = [((# #), TYPE ('TupleRep '[])),
((# #), TYPE ('TupleRep '[])), (a_au1, (# #)), ('(), (# #))]
Forall: k1_11
*
((# #), TYPE ('TupleRep '[]))
In the type of a binder: MkS
In the type ‘forall (a :: (# #)). (a ~# '()) > S a’
Substitution: [TCvSubst
In scope: InScope {a_au1 $WMkS}
Type env: []
Co env: []]
Bug.hs:11:1: warning:
Kind application error in type ‘a_au1 ~# '()’
Function kind = forall k0 k1. k0 > k1 > TYPE ('TupleRep '[])
Arg kinds = [((# #), TYPE ('TupleRep '[])),
((# #), TYPE ('TupleRep '[])), (a_au1, (# #)), ('(), (# #))]
Forall: k0_10
*
((# #), TYPE ('TupleRep '[]))
In the RHS of MkS :: forall (a :: (# #)). (a ~# '()) > S a
In the body of lambda with binder a_au1 :: (# #)
In the body of lambda with binder eta_B1 :: a_au1 ~# '()
Substitution: [TCvSubst
In scope: InScope {a_au1 $WMkS MkS}
Type env: []
Co env: []]
Bug.hs:11:1: warning:
Kind application error in type ‘a_au1 ~# '()’
Function kind = forall k0 k1. k0 > k1 > TYPE ('TupleRep '[])
Arg kinds = [((# #), TYPE ('TupleRep '[])),
((# #), TYPE ('TupleRep '[])), (a_au1, (# #)), ('(), (# #))]
Forall: k1_11
*
((# #), TYPE ('TupleRep '[]))
In the RHS of MkS :: forall (a :: (# #)). (a ~# '()) > S a
In the body of lambda with binder a_au1 :: (# #)
In the body of lambda with binder eta_B1 :: a_au1 ~# '()
Substitution: [TCvSubst
In scope: InScope {a_au1 $WMkS MkS}
Type env: []
Co env: []]
*** Offending Program ***
$WMkS [InlPrag=INLINE[0]] :: S '()
[GblId[DataConWrapper], Caf=NoCafRefs, Str=m, Unf=OtherCon []]
$WMkS = MkS @ '() @~ (<'()>_N :: '() ~# '())
MkS :: forall (a :: (# #)). (a ~# '()) > S a
[GblId[DataCon],
Arity=1,
Caf=NoCafRefs,
Str=<L,U>m,
Unf=OtherCon []]
MkS
= \ (@ (a_au1 :: (# #))) (eta_B1 :: a_au1 ~# '()) >
MkS @ a_au1 @~ (eta_B1 :: a_au1 ~# '())
*** End of Offense ***
<no location info>: error:
Compilation had errors
```
Note that if you tried to inline the `UT` type synonym's definition, like so:
```hs
data S :: (##) > Type where
MkS :: S '(##)
```
Then GHC's typechecker would reject it:
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:11: error:
• Expecting a lifted type, but ‘(# #)’ is unlifted
• In the kind ‘(# #) > Type’
In the data type declaration for ‘S’

11  data S :: (##) > Type where
 ^^^^
```
This is because `(>)` has different typing rules depending on whether it is used in a type or kind position, as explained [here](https://gitlab.haskell.org/ghc/ghc//issues/14180#note_158783). In a type position, `(>)` is levity polymorphic in its arguments, but in a kind position, it is not. GHC treats the RHS of a type synonyms as a type position, so it happy accepts `type UT = (##) > Type`. When `UT` is later used in a kind position like `data S :: UT`, however, things go awry.
One way to fix this bug would be to fix #14180. But that would likely be a lot of work, so perhaps there is a way to at least cause this program not to typecheck in the meantime?#14180 says that levity polymorphism in kinds isn't possible right now. Actually, this is only half true: it's possible if you leverage a backdoor. This backdoor is known as type synonyms:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE UnboxedTuples #}
{# OPTIONS_GHC dcorelint #}
module Bug where
import Data.Kind
type UT = (##) > Type
data S :: UT where
MkS :: S '(##)
```
This program, when compiled with GHC 8.0 or later, will produce a Core Lint error. Here is the error on 8.10.2:
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs dnotypeablebinds
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of CorePrep ***
Bug.hs:12:3: warning:
Kind application error in type ‘a_au1 ~# '()’
Function kind = forall k0 k1. k0 > k1 > TYPE ('TupleRep '[])
Arg kinds = [((# #), TYPE ('TupleRep '[])),
((# #), TYPE ('TupleRep '[])), (a_au1, (# #)), ('(), (# #))]
Forall: k0_10
*
((# #), TYPE ('TupleRep '[]))
In the type of a binder: MkS
In the type ‘forall (a :: (# #)). (a ~# '()) > S a’
Substitution: [TCvSubst
In scope: InScope {a_au1 $WMkS}
Type env: []
Co env: []]
Bug.hs:12:3: warning:
Kind application error in type ‘a_au1 ~# '()’
Function kind = forall k0 k1. k0 > k1 > TYPE ('TupleRep '[])
Arg kinds = [((# #), TYPE ('TupleRep '[])),
((# #), TYPE ('TupleRep '[])), (a_au1, (# #)), ('(), (# #))]
Forall: k1_11
*
((# #), TYPE ('TupleRep '[]))
In the type of a binder: MkS
In the type ‘forall (a :: (# #)). (a ~# '()) > S a’
Substitution: [TCvSubst
In scope: InScope {a_au1 $WMkS}
Type env: []
Co env: []]
Bug.hs:11:1: warning:
Kind application error in type ‘a_au1 ~# '()’
Function kind = forall k0 k1. k0 > k1 > TYPE ('TupleRep '[])
Arg kinds = [((# #), TYPE ('TupleRep '[])),
((# #), TYPE ('TupleRep '[])), (a_au1, (# #)), ('(), (# #))]
Forall: k0_10
*
((# #), TYPE ('TupleRep '[]))
In the RHS of MkS :: forall (a :: (# #)). (a ~# '()) > S a
In the body of lambda with binder a_au1 :: (# #)
In the body of lambda with binder eta_B1 :: a_au1 ~# '()
Substitution: [TCvSubst
In scope: InScope {a_au1 $WMkS MkS}
Type env: []
Co env: []]
Bug.hs:11:1: warning:
Kind application error in type ‘a_au1 ~# '()’
Function kind = forall k0 k1. k0 > k1 > TYPE ('TupleRep '[])
Arg kinds = [((# #), TYPE ('TupleRep '[])),
((# #), TYPE ('TupleRep '[])), (a_au1, (# #)), ('(), (# #))]
Forall: k1_11
*
((# #), TYPE ('TupleRep '[]))
In the RHS of MkS :: forall (a :: (# #)). (a ~# '()) > S a
In the body of lambda with binder a_au1 :: (# #)
In the body of lambda with binder eta_B1 :: a_au1 ~# '()
Substitution: [TCvSubst
In scope: InScope {a_au1 $WMkS MkS}
Type env: []
Co env: []]
*** Offending Program ***
$WMkS [InlPrag=INLINE[0]] :: S '()
[GblId[DataConWrapper], Caf=NoCafRefs, Str=m, Unf=OtherCon []]
$WMkS = MkS @ '() @~ (<'()>_N :: '() ~# '())
MkS :: forall (a :: (# #)). (a ~# '()) > S a
[GblId[DataCon],
Arity=1,
Caf=NoCafRefs,
Str=<L,U>m,
Unf=OtherCon []]
MkS
= \ (@ (a_au1 :: (# #))) (eta_B1 :: a_au1 ~# '()) >
MkS @ a_au1 @~ (eta_B1 :: a_au1 ~# '())
*** End of Offense ***
<no location info>: error:
Compilation had errors
```
Note that if you tried to inline the `UT` type synonym's definition, like so:
```hs
data S :: (##) > Type where
MkS :: S '(##)
```
Then GHC's typechecker would reject it:
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:11: error:
• Expecting a lifted type, but ‘(# #)’ is unlifted
• In the kind ‘(# #) > Type’
In the data type declaration for ‘S’

11  data S :: (##) > Type where
 ^^^^
```
This is because `(>)` has different typing rules depending on whether it is used in a type or kind position, as explained [here](https://gitlab.haskell.org/ghc/ghc//issues/14180#note_158783). In a type position, `(>)` is levity polymorphic in its arguments, but in a kind position, it is not. GHC treats the RHS of a type synonyms as a type position, so it happy accepts `type UT = (##) > Type`. When `UT` is later used in a kind position like `data S :: UT`, however, things go awry.
One way to fix this bug would be to fix #14180. But that would likely be a lot of work, so perhaps there is a way to at least cause this program not to typecheck in the meantime?https://gitlab.haskell.org/ghc/ghc//issues/17201Levity polymorphism and defaulting20200924T16:34:02ZKrzysztof GogolewskiLevity polymorphism and defaultingThis ticket concerns two closely related items regarding levity polymorphism.
1. Consider
```
f1 :: forall (p :: RuntimeRep > Type) (r :: RuntimeRep). p r > p r
f1 x = x
 Inferred type g1 :: forall (p :: RuntimeRep > Type). p 'LiftedRep > p 'LiftedRep
g1 = f1
f2 :: (p :: Bool > Type) (r :: Bool). p r > p r
f2 x = x
 Inferred type g2 :: forall (p :: Bool > Type) (r :: Bool). p r > p r
g2 = f2
f3 :: forall k (p :: k > Type) (r :: k). p r > p r
f3 x = x
 Inferred type g3 :: forall k (p :: k > Type) (r :: k). p r > p r
g3 = f3
type family R
type instance R = RuntimeRep
f4 :: (p :: R> Type) (r :: R). p r > p r
f2 x = x
 Inferred type g4 :: forall (p :: R > Type) (r :: R). p r > p r
g4 = f4
```
As you can see `g1` gets a less general type than `g2`, but the only difference is `RuntimeRep` vs `Bool`.
And `g3` also gets a more general type, even though `k` could be instantiated to `RuntimeRep` in a call.
And `g4` disguises `RuntimeRep` behind a type family, and so becomes polymorphic.
This inconsistency is all pretty disgusting.
Proposed alternative:
* When we typecheck a binder, we unify the kind of its type with `TYPE q`, and emit a new constraint `StaticRuntimeRep q`. Similarly for other places where levity polymorphsm
* Never generalise over `StaticRuntimeRep` constraints.
* Default any unsolved `StaticRuntimeRep` constraints at the end.
That could even be connected the defaulting mechanism, so that you could say `default (UnliftedRep)` in a module, or `default (One)` for multiplicity polymorphism in linear types.
Richard says that a lot of machinery for `TypeLike` (#15979) will overlap with this ticket.
2. Consider
```
f x = x
g = f 0#
```
Currently, when `f` is typechecked, it's argument is inferred to be lifted, and typechecking of `g` fails. An alternative strategy is to mimic monomorphism restriction. Rather than *defaulting*
RuntimeRep varaibles in `TcMType.defaultTyVar`, simply *refrain from quantifying over it*. The type of `f` would be `forall (a :: TYPE q). a > a`, where `q` is a free unification variable.
This ticket concerns two closely related items regarding levity polymorphism.
1. Consider
```
f1 :: forall (p :: RuntimeRep > Type) (r :: RuntimeRep). p r > p r
f1 x = x
 Inferred type g1 :: forall (p :: RuntimeRep > Type). p 'LiftedRep > p 'LiftedRep
g1 = f1
f2 :: (p :: Bool > Type) (r :: Bool). p r > p r
f2 x = x
 Inferred type g2 :: forall (p :: Bool > Type) (r :: Bool). p r > p r
g2 = f2
f3 :: forall k (p :: k > Type) (r :: k). p r > p r
f3 x = x
 Inferred type g3 :: forall k (p :: k > Type) (r :: k). p r > p r
g3 = f3
type family R
type instance R = RuntimeRep
f4 :: (p :: R> Type) (r :: R). p r > p r
f2 x = x
 Inferred type g4 :: forall (p :: R > Type) (r :: R). p r > p r
g4 = f4
```
As you can see `g1` gets a less general type than `g2`, but the only difference is `RuntimeRep` vs `Bool`.
And `g3` also gets a more general type, even though `k` could be instantiated to `RuntimeRep` in a call.
And `g4` disguises `RuntimeRep` behind a type family, and so becomes polymorphic.
This inconsistency is all pretty disgusting.
Proposed alternative:
* When we typecheck a binder, we unify the kind of its type with `TYPE q`, and emit a new constraint `StaticRuntimeRep q`. Similarly for other places where levity polymorphsm
* Never generalise over `StaticRuntimeRep` constraints.
* Default any unsolved `StaticRuntimeRep` constraints at the end.
That could even be connected the defaulting mechanism, so that you could say `default (UnliftedRep)` in a module, or `default (One)` for multiplicity polymorphism in linear types.
Richard says that a lot of machinery for `TypeLike` (#15979) will overlap with this ticket.
2. Consider
```
f x = x
g = f 0#
```
Currently, when `f` is typechecked, it's argument is inferred to be lifted, and typechecking of `g` fails. An alternative strategy is to mimic monomorphism restriction. Rather than *defaulting*
RuntimeRep varaibles in `TcMType.defaultTyVar`, simply *refrain from quantifying over it*. The type of `f` would be `forall (a :: TYPE q). a > a`, where `q` is a free unification variable.
https://gitlab.haskell.org/ghc/ghc//issues/14180Permit levity polymorphism in kinds20200916T18:18:18ZDavid FeuerPermit levity polymorphism in kinds```hs
{# language TypeInType, TypeFamilies, MagicHash #}
import GHC.Exts
type family MatchInt (f :: Int) :: () where
MatchInt ('I# x) = '()
```
produces
```
<interactive>:2:59: error:
• Couldn't match a lifted type with an unlifted type
When matching kinds
k0 :: *
Int# :: TYPE 'IntRep
Expected kind ‘Int#’, but ‘x’ has kind ‘k0’
• In the first argument of ‘ 'I#’, namely ‘x’
In the first argument of ‘MatchInt’, namely ‘( 'I# x)’
In the type family declaration for ‘MatchInt’
```
If, however, I replace `x` in the pattern with `_`, the type checker is satisfied. If I give it a pattern signature,
```hs
MatchInt ('I# (x :: Int#)) = '()
```
I get a different (and equally unhelpful) error message,
```
• Expecting a lifted type, but ‘Int#’ is unlifted
• In the kind ‘Int#’
In the first argument of ‘ 'I#’, namely ‘(x :: Int#)’
In the first argument of ‘MatchInt’, namely ‘( 'I# (x :: Int#))’
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Strange/bad error message binding unboxed type variable","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.2","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# language TypeInType, TypeFamilies, MagicHash #}\r\n\r\nimport GHC.Exts\r\n\r\ntype family MatchInt (f :: Int) :: () where\r\n MatchInt ('I# x) = '()\r\n}}}\r\n\r\nproduces\r\n\r\n{{{\r\n<interactive>:2:59: error:\r\n • Couldn't match a lifted type with an unlifted type\r\n When matching kinds\r\n k0 :: *\r\n Int# :: TYPE 'IntRep\r\n Expected kind ‘Int#’, but ‘x’ has kind ‘k0’\r\n • In the first argument of ‘ 'I#’, namely ‘x’\r\n In the first argument of ‘MatchInt’, namely ‘( 'I# x)’\r\n In the type family declaration for ‘MatchInt’\r\n}}}\r\n\r\nIf, however, I replace `x` in the pattern with `_`, the type checker is satisfied. If I give it a pattern signature,\r\n\r\n{{{#!hs\r\nMatchInt ('I# (x :: Int#)) = '()\r\n}}}\r\n\r\nI get a different (and equally unhelpful) error message,\r\n\r\n{{{\r\n • Expecting a lifted type, but ‘Int#’ is unlifted\r\n • In the kind ‘Int#’\r\n In the first argument of ‘ 'I#’, namely ‘(x :: Int#)’\r\n In the first argument of ‘MatchInt’, namely ‘( 'I# (x :: Int#))’\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >```hs
{# language TypeInType, TypeFamilies, MagicHash #}
import GHC.Exts
type family MatchInt (f :: Int) :: () where
MatchInt ('I# x) = '()
```
produces
```
<interactive>:2:59: error:
• Couldn't match a lifted type with an unlifted type
When matching kinds
k0 :: *
Int# :: TYPE 'IntRep
Expected kind ‘Int#’, but ‘x’ has kind ‘k0’
• In the first argument of ‘ 'I#’, namely ‘x’
In the first argument of ‘MatchInt’, namely ‘( 'I# x)’
In the type family declaration for ‘MatchInt’
```
If, however, I replace `x` in the pattern with `_`, the type checker is satisfied. If I give it a pattern signature,
```hs
MatchInt ('I# (x :: Int#)) = '()
```
I get a different (and equally unhelpful) error message,
```
• Expecting a lifted type, but ‘Int#’ is unlifted
• In the kind ‘Int#’
In the first argument of ‘ 'I#’, namely ‘(x :: Int#)’
In the first argument of ‘MatchInt’, namely ‘( 'I# (x :: Int#))’
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Strange/bad error message binding unboxed type variable","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.2","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# language TypeInType, TypeFamilies, MagicHash #}\r\n\r\nimport GHC.Exts\r\n\r\ntype family MatchInt (f :: Int) :: () where\r\n MatchInt ('I# x) = '()\r\n}}}\r\n\r\nproduces\r\n\r\n{{{\r\n<interactive>:2:59: error:\r\n • Couldn't match a lifted type with an unlifted type\r\n When matching kinds\r\n k0 :: *\r\n Int# :: TYPE 'IntRep\r\n Expected kind ‘Int#’, but ‘x’ has kind ‘k0’\r\n • In the first argument of ‘ 'I#’, namely ‘x’\r\n In the first argument of ‘MatchInt’, namely ‘( 'I# x)’\r\n In the type family declaration for ‘MatchInt’\r\n}}}\r\n\r\nIf, however, I replace `x` in the pattern with `_`, the type checker is satisfied. If I give it a pattern signature,\r\n\r\n{{{#!hs\r\nMatchInt ('I# (x :: Int#)) = '()\r\n}}}\r\n\r\nI get a different (and equally unhelpful) error message,\r\n\r\n{{{\r\n • Expecting a lifted type, but ‘Int#’ is unlifted\r\n • In the kind ‘Int#’\r\n In the first argument of ‘ 'I#’, namely ‘(x :: Int#)’\r\n In the first argument of ‘MatchInt’, namely ‘( 'I# (x :: Int#))’\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/17670Levitypolymorphism checker is too aggressive for uses of `coerce` on levity...20200619T14:05:21ZAlexis KingLevitypolymorphism checker is too aggressive for uses of `coerce` on levitypolymorphic newtypesGHC 8.10.1alpha2 rejects this program:
```haskell
{# LANGUAGE DataKinds, FlexibleContexts, MagicHash, PolyKinds, RankNTypes, StandaloneKindSignatures, TypeFamilies, UnliftedNewtypes #}
module M where
import Data.Coerce
import Data.Kind
import GHC.Exts (RuntimeRep(..), TYPE)
type UnboxedRep :: Type > RuntimeRep
type family UnboxedRep a
type Unboxed :: forall (a :: Type) > TYPE (UnboxedRep a)
type family Unboxed a
 The above definitions allow us to define, say
 type instance UnboxedRep Int = 'IntRep
 type instance Unboxed Int = Int#
 but those definitions are not necessary for this issue.
newtype N a = N (Unboxed a)
unN :: Coercible (N a) (Unboxed a) => N a > Unboxed a
unN = coerce
```
```
M.hs:22:7: error:
Cannot use function with levitypolymorphic arguments:
coerce :: N a > Unboxed a
Levitypolymorphic arguments: N a :: TYPE (UnboxedRep a)

22  unN = coerce
 ^^^^^^
```
I think the program ought to be accepted. There are no levitypolymorphic arguments here; surely the code generator has no trouble with `unN`, which simply returns a function? Indeed, both of the following definitions are accepted:
```haskell
f :: (N a > Unboxed a) > N a > Unboxed a
f = id
type C :: TYPE r1 > TYPE r2 > Constraint
class C a b where
m :: a > b
g :: C (N a) (Unboxed a) => N a > Unboxed a
g = m
```
Even more bizarre, the following instance of `C` is accepted, too:
```haskell
instance Coercible a b => C a b where
m = coerce
```
So I have no idea why `unN` is rejected, but it seems like something funny is going on with `coerce`.GHC 8.10.1alpha2 rejects this program:
```haskell
{# LANGUAGE DataKinds, FlexibleContexts, MagicHash, PolyKinds, RankNTypes, StandaloneKindSignatures, TypeFamilies, UnliftedNewtypes #}
module M where
import Data.Coerce
import Data.Kind
import GHC.Exts (RuntimeRep(..), TYPE)
type UnboxedRep :: Type > RuntimeRep
type family UnboxedRep a
type Unboxed :: forall (a :: Type) > TYPE (UnboxedRep a)
type family Unboxed a
 The above definitions allow us to define, say
 type instance UnboxedRep Int = 'IntRep
 type instance Unboxed Int = Int#
 but those definitions are not necessary for this issue.
newtype N a = N (Unboxed a)
unN :: Coercible (N a) (Unboxed a) => N a > Unboxed a
unN = coerce
```
```
M.hs:22:7: error:
Cannot use function with levitypolymorphic arguments:
coerce :: N a > Unboxed a
Levitypolymorphic arguments: N a :: TYPE (UnboxedRep a)

22  unN = coerce
 ^^^^^^
```
I think the program ought to be accepted. There are no levitypolymorphic arguments here; surely the code generator has no trouble with `unN`, which simply returns a function? Indeed, both of the following definitions are accepted:
```haskell
f :: (N a > Unboxed a) > N a > Unboxed a
f = id
type C :: TYPE r1 > TYPE r2 > Constraint
class C a b where
m :: a > b
g :: C (N a) (Unboxed a) => N a > Unboxed a
g = m
```
Even more bizarre, the following instance of `C` is accepted, too:
```haskell
instance Coercible a b => C a b where
m = coerce
```
So I have no idea why `unN` is rejected, but it seems like something funny is going on with `coerce`.https://gitlab.haskell.org/ghc/ghc//issues/13105Allow type families in RuntimeReps20200513T18:21:12ZRichard Eisenbergrae@richarde.devAllow type families in RuntimeRepsConal 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 wholeprogram 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.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Allow type families in RuntimeReps","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Conal Elliott provided me with this puzzle:\r\n\r\n{{{\r\ntype family RepRep a ∷ RuntimeRep\r\n\r\nclass HasRep a where\r\n type Rep a ∷ TYPE (RepRep a)\r\n repr ∷ a → Rep a\r\n abst ∷ Rep a → a\r\n\r\ntype instance RepRep Int = IntRep\r\n\r\ninstance HasRep Int where\r\n type Rep Int = Int#\r\n abst n = I# n\r\n repr (I# n) = n\r\n}}}\r\n\r\nI 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.\r\n\r\nThe solution here is either to teach the code generator how to normalise types (requiring propagating the `FamInstEnvs`) or to do a wholeprogram 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`.\r\n\r\nBut 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.","type_of_failure":"OtherFailure","blocking":[]} >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 wholeprogram 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.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Allow type families in RuntimeReps","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Conal Elliott provided me with this puzzle:\r\n\r\n{{{\r\ntype family RepRep a ∷ RuntimeRep\r\n\r\nclass HasRep a where\r\n type Rep a ∷ TYPE (RepRep a)\r\n repr ∷ a → Rep a\r\n abst ∷ Rep a → a\r\n\r\ntype instance RepRep Int = IntRep\r\n\r\ninstance HasRep Int where\r\n type Rep Int = Int#\r\n abst n = I# n\r\n repr (I# n) = n\r\n}}}\r\n\r\nI 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.\r\n\r\nThe solution here is either to teach the code generator how to normalise types (requiring propagating the `FamInstEnvs`) or to do a wholeprogram 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`.\r\n\r\nBut 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.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/17675eqType fails on comparing FunTys20200502T22:16:29ZRichard Eisenbergrae@richarde.deveqType fails on comparing FunTysSuppose I have `co :: IntRep ~ r` and `a :: TYPE IntRep`. Consider `t1 = a > ()` and `t2 = (a > TYPE co) > ()`. We have ``t1 `eqType` t2``, but if we call `splitTyConApp` on `t1` and `t2`, we'll get different arguments (the first arg in `t1` will be `IntRep` while the first arg in `t2` will be `r`). This violates property EQ of Note [Nontrivial definitional equality] in TyCoRep.
The fix is easy: in `nonDetCmpTypeX`, the `FunTy` case should recur into `nonDetCmpTypeX` for both argument and result. This does a kind check. Recurring into `go` skips the kind check.
Unfortunately, there are other places that also work with equality. This list includes at least
* [ ] `TcType.tc_eq_type`
* [ ] `CoreMap`
* [ ] Pure unifier in `Unify`, which probably also needs to recur in kinds on a `FunTy`. Or maybe this works via decomposition into a `TyConApp`, so all is OK. But it needs to be checked.
I believe Simon has some preliminary work on a branch.Suppose I have `co :: IntRep ~ r` and `a :: TYPE IntRep`. Consider `t1 = a > ()` and `t2 = (a > TYPE co) > ()`. We have ``t1 `eqType` t2``, but if we call `splitTyConApp` on `t1` and `t2`, we'll get different arguments (the first arg in `t1` will be `IntRep` while the first arg in `t2` will be `r`). This violates property EQ of Note [Nontrivial definitional equality] in TyCoRep.
The fix is easy: in `nonDetCmpTypeX`, the `FunTy` case should recur into `nonDetCmpTypeX` for both argument and result. This does a kind check. Recurring into `go` skips the kind check.
Unfortunately, there are other places that also work with equality. This list includes at least
* [ ] `TcType.tc_eq_type`
* [ ] `CoreMap`
* [ ] Pure unifier in `Unify`, which probably also needs to recur in kinds on a `FunTy`. Or maybe this works via decomposition into a `TyConApp`, so all is OK. But it needs to be checked.
I believe Simon has some preliminary work on a branch.https://gitlab.haskell.org/ghc/ghc//issues/18080Eliminate excessive RuntimeRep polymorphism in primops20200422T16:31:29ZBen GamariEliminate excessive RuntimeRep polymorphism in primopsCurrently there are numerous primops whose types are parametrically polymorphic in `RuntimeRep` yet only work with pointers (namely `LiftedPtrRep` and `UnliftedPtrRep`). This uneasy situation is forced by the fact that we currently don't have a convenient way to distinguish pointers from nonpointers. #17526 (GHC proposal 203) replaces the `LiftedPtrRep` and `UnliftedPtrRep` constructors of `RuntimeRep` with a `BoxedRep :: Levity > RuntimeRep` constructor. This will allow us to give the correct types to the following primops:
* [ ] `mkWeak#` and `mkWeakNoFinalizer#`
* [ ] `touch#`
* [ ] `keepAlive#` (once it's merged; see #17760)
Implementing this idea depends on completing !2249 (BoxedRep)Currently there are numerous primops whose types are parametrically polymorphic in `RuntimeRep` yet only work with pointers (namely `LiftedPtrRep` and `UnliftedPtrRep`). This uneasy situation is forced by the fact that we currently don't have a convenient way to distinguish pointers from nonpointers. #17526 (GHC proposal 203) replaces the `LiftedPtrRep` and `UnliftedPtrRep` constructors of `RuntimeRep` with a `BoxedRep :: Levity > RuntimeRep` constructor. This will allow us to give the correct types to the following primops:
* [ ] `mkWeak#` and `mkWeakNoFinalizer#`
* [ ] `touch#`
* [ ] `keepAlive#` (once it's merged; see #17760)
Implementing this idea depends on completing !2249 (BoxedRep)https://gitlab.haskell.org/ghc/ghc//issues/17723Using default methods with (r ~ LiftedRep) leads to Iface Lint failure20200416T12:01:30ZRyan ScottUsing default methods with (r ~ LiftedRep) leads to Iface Lint failureI originally spotted this bug when trying to minimize #17722, but I believe this is an entirely different bug. To reproduce the issue, you'll need these two files:
```hs
 Lib.hs
{# LANGUAGE DataKinds #}
{# LANGUAGE DefaultSignatures #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Lib (C(..)) where
import GHC.Exts
 Essentially a strippeddown version of the `Lift` type class from
 Language.Haskell.TH.Syntax. I have redefined it here both to strip away
 inessential details and to ensure that this test case will not change if
 the API of Lift were to change in the future.
class C (a :: TYPE (r :: RuntimeRep)) where
m :: a > ()
default m :: (r ~ LiftedRep) => a > ()
m = const ()
```
```hs
 Bug.hs
module Bug where
import Lib
data Foo
instance C Foo
```
Next, compile them with a recent version of GHC like so:
```
$ /opt/ghc/8.8.2/bin/ghc c Lib.hs O dcorelint && /opt/ghc/8.8.2/bin/ghc c Bug.hs O dcorelint
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.2 for x86_64unknownlinux):
Iface Lint failure
In interface for Lib
Unfolding of $dmm
<no location info>: warning:
In the type ‘(a_a1a9 > Sym (TYPE (Sym co_a1ac))_N) > ()’
co_a1ac :: r_a1a8 ~# 'LiftedRep
[LclId[CoVarId]] is out of scope
$dmm = \ (@ (r_a1a8 :: RuntimeRep))
(@ (a_a1a9 :: TYPE r_a1a8))
($dC_a1aa :: C a_a1a9)
($d~_a1ab :: r_a1a8 ~ 'LiftedRep) >
case eq_sel @ RuntimeRep @ r_a1a8 @ 'LiftedRep $d~_a1ab of co_a1ac
{ __DEFAULT >
\ (ds_a1ad :: (a_a1a9 > Sym (TYPE (Sym co_a1ac))_N)) > ()
}
Iface expr = \ @ r :: RuntimeRep
@ a :: TYPE r
($dC :: C a)
($d~ :: r ~ 'LiftedRep) >
case eq_sel @ RuntimeRep @ r @ 'LiftedRep $d~ of co { DEFAULT >
\ (ds :: (a > Sym (TYPE (Sym co))_N)) > () }
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/iface/TcIface.hs:1546:33 in ghc:TcIface
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
I have observed this panic on every version of GHC from 8.2.2 to HEAD.
Another strange thing about this program is that I have to write `m = const ()`. If I instead try to define it like `m _ = ()`, I get the following error:
```
$ /opt/ghc/8.8.2/bin/ghc c Lib.hs O dcorelint && /opt/ghc/8.8.2/bin/ghc c Bug.hs O dcorelint
Lib.hs:19:5: error:
A levitypolymorphic type is not allowed here:
Type: a
Kind: TYPE r
In a wildcard pattern

19  m _ = ()
 ^
```
This seems suspicious, does it not? Why should that binder get rejected for being levity polymorphic if `r ~ LiftedRep`? Shouldn't that make the binder levity monomorphic?I originally spotted this bug when trying to minimize #17722, but I believe this is an entirely different bug. To reproduce the issue, you'll need these two files:
```hs
 Lib.hs
{# LANGUAGE DataKinds #}
{# LANGUAGE DefaultSignatures #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Lib (C(..)) where
import GHC.Exts
 Essentially a strippeddown version of the `Lift` type class from
 Language.Haskell.TH.Syntax. I have redefined it here both to strip away
 inessential details and to ensure that this test case will not change if
 the API of Lift were to change in the future.
class C (a :: TYPE (r :: RuntimeRep)) where
m :: a > ()
default m :: (r ~ LiftedRep) => a > ()
m = const ()
```
```hs
 Bug.hs
module Bug where
import Lib
data Foo
instance C Foo
```
Next, compile them with a recent version of GHC like so:
```
$ /opt/ghc/8.8.2/bin/ghc c Lib.hs O dcorelint && /opt/ghc/8.8.2/bin/ghc c Bug.hs O dcorelint
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.2 for x86_64unknownlinux):
Iface Lint failure
In interface for Lib
Unfolding of $dmm
<no location info>: warning:
In the type ‘(a_a1a9 > Sym (TYPE (Sym co_a1ac))_N) > ()’
co_a1ac :: r_a1a8 ~# 'LiftedRep
[LclId[CoVarId]] is out of scope
$dmm = \ (@ (r_a1a8 :: RuntimeRep))
(@ (a_a1a9 :: TYPE r_a1a8))
($dC_a1aa :: C a_a1a9)
($d~_a1ab :: r_a1a8 ~ 'LiftedRep) >
case eq_sel @ RuntimeRep @ r_a1a8 @ 'LiftedRep $d~_a1ab of co_a1ac
{ __DEFAULT >
\ (ds_a1ad :: (a_a1a9 > Sym (TYPE (Sym co_a1ac))_N)) > ()
}
Iface expr = \ @ r :: RuntimeRep
@ a :: TYPE r
($dC :: C a)
($d~ :: r ~ 'LiftedRep) >
case eq_sel @ RuntimeRep @ r @ 'LiftedRep $d~ of co { DEFAULT >
\ (ds :: (a > Sym (TYPE (Sym co))_N)) > () }
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/iface/TcIface.hs:1546:33 in ghc:TcIface
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
I have observed this panic on every version of GHC from 8.2.2 to HEAD.
Another strange thing about this program is that I have to write `m = const ()`. If I instead try to define it like `m _ = ()`, I get the following error:
```
$ /opt/ghc/8.8.2/bin/ghc c Lib.hs O dcorelint && /opt/ghc/8.8.2/bin/ghc c Bug.hs O dcorelint
Lib.hs:19:5: error:
A levitypolymorphic type is not allowed here:
Type: a
Kind: TYPE r
In a wildcard pattern

19  m _ = ()
 ^
```
This seems suspicious, does it not? Why should that binder get rejected for being levity polymorphic if `r ~ LiftedRep`? Shouldn't that make the binder levity monomorphic?https://gitlab.haskell.org/ghc/ghc//issues/15532Relaxing LevityPolymorphic Binder Check for Lifted vs Unlifted pointers20200319T20:42:54ZAndrew MartinRelaxing LevityPolymorphic Binder Check for Lifted vs Unlifted pointersI'm going to define two terms that I will use with these meanings for the remainder of this post.
1. RuntimeRep Polymorphism: full polymorphism in the runtime representation
1. Levity Polymorphism: polymorphism dealing with lifted vs unlifted types that are definitely represented by pointers.
GHC's levity polymorphism has the restriction that runtimereppolymorphic binders are not allowed. A comment David made recently on https://github.com/haskell/primitive/issues/198 got me thinking about the possibility of relaxing this restriction when it comes to dealing with a function with levitypolymorphic (not runtimereppolymorphic) binders. GHC's runtime already appears to allow doing this. AndrasKovacs writes on https://www.reddit.com/r/haskell/comments/6v9rmg/an_unified_array_interface/dlyug4e/ that he is able to store both lifted and unlifted values inside of the same `Array#` (pointing out as well that their primop implementations are identical) without crashing the GC. As further evidence that we can, roughly speaking, use lifted and unlifted values in the same places, I threw together a little experiment:
```
{# LANGUAGE MagicHash #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
import Data.Primitive
import Data.Primitive.UnliftedArray
import GHC.Types
import GHC.Exts
main :: IO ()
main = do
a@(Array myArr) < newArray 1 ("foo" :: String) >>= unsafeFreezeArray
UnliftedArray myArrArr < newUnliftedArray 1 a >>= unsafeFreezeUnliftedArray
putStrLn (myFunc show (2 :: Integer))
putStrLn (myFunc2 (\x > show (Array x)) myArr)
putStrLn (myBigFunc (+1) show show (2 :: Integer))
putStrLn (myBigFunc2 (\x > array# (indexUnliftedArray (UnliftedArray x) 0 :: Array String)) (\x > show (Array x)) (\x > show (UnliftedArray x :: UnliftedArray (Array String))) myArrArr)
{# NOINLINE myFunc #}
myFunc :: (a > String) > a > String
myFunc f a =
let x = f a
in x ++ x
myFunc2 :: forall (a :: TYPE 'UnliftedRep). (a > String) > a > String
myFunc2 = unsafeCoerce# myFunc
{# NOINLINE myBigFunc #}
myBigFunc :: (a > b) > (b > String) > (a > String) > a > String
myBigFunc f g h a =
let y = f a
x = g y
in x ++ x ++ h a
myBigFunc2 :: forall (a :: TYPE 'UnliftedRep) (b :: TYPE 'UnliftedRep). (a > b) > (b > String) > (a > String) > a > String
myBigFunc2 = unsafeCoerce# myBigFunc
```
The compiles (surprisingly without a core lint error) and runs fine. So, here's the idea. We start with David's suggested change to `RuntimeRep`:
```
data RuntimeRep
= PtrRep Levity
 ...
data Levity = Lifted  Unlifted
```
And then we change the check that disallows runtimerep polymorphism in binding positions to accept levity polymorphism in binding positions (but continuing to reject runtimerep polymorphism). For example, the two examples in the above code snippet would be rewritten as:
```
myFunc :: forall (v :: Levity) (a :: TYPE ('PtrRep v)). (a > String) > a > String
myFunc = ...  same implementation
myBigFunc :: forall (v :: Levity) (w :: Levity) (a :: TYPE ('PtrRep v)) (b :: TYPE ('PtrRep w)). (a > b) > (b > String) > (a > String) > a > String
myBigFunc = ...  same implementation
```
Again, GHC's runtime seems to already allow this. It's just the type system that's missing support for it. The only weird thing I can think of that comes up is that you cannot use bang patterns on a levitypolymorphic argument since unlifted values cannot be entered.
I think it is possible to go a little further still. Fields of data types could be levity polymorphic:
```
data List (a :: TYPE ('PtrRep v)) = Cons a (List a)  Nil
map :: forall (v :: Levity) (w :: Levity) (a :: TYPE ('PtrRep v)) (b :: TYPE ('PtrRep w)). (a > b) > List a > List b
```
Again, bang patterns would need to be forbidden on such fields. This doesn't get us everything sought out in https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes, but it's kind of a halfway point that requires no changes to GHC's runtime and no changes to code generation. I think the whole thing can be handled in the type checker. Other potential application: `Array#` and `ArrayArray#` (and nearly all functions that operate on them) could be consolidated into a single type, reducing the number of duplicated primop implementations in GHC.
Of course this would all need to be a GHC proposal, but I wanted to first solicit some feedback here on initial draft of the idea.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  dfeuer, goldfirere, simonpj, treeowl 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Relaxing LevityPolymorphic Binder Check for Lifted vs Unlifted pointers","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["LevityPolymorphism"],"differentials":[],"test_case":"","architecture":"","cc":["dfeuer","goldfirere","simonpj","treeowl"],"type":"FeatureRequest","description":"I'm going to define two terms that I will use with these meanings for the remainder of this post.\r\n\r\n1. RuntimeRep Polymorphism: full polymorphism in the runtime representation\r\n2. Levity Polymorphism: polymorphism dealing with lifted vs unlifted types that are definitely represented by pointers.\r\n\r\nGHC's levity polymorphism has the restriction that runtimereppolymorphic binders are not allowed. A comment David made recently on https://github.com/haskell/primitive/issues/198 got me thinking about the possibility of relaxing this restriction when it comes to dealing with a function with levitypolymorphic (not runtimereppolymorphic) binders. GHC's runtime already appears to allow doing this. AndrasKovacs writes on https://www.reddit.com/r/haskell/comments/6v9rmg/an_unified_array_interface/dlyug4e/ that he is able to store both lifted and unlifted values inside of the same `Array#` (pointing out as well that their primop implementations are identical) without crashing the GC. As further evidence that we can, roughly speaking, use lifted and unlifted values in the same places, I threw together a little experiment:\r\n\r\n{{{\r\n{# LANGUAGE MagicHash #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeInType #}\r\n\r\nimport Data.Primitive\r\nimport Data.Primitive.UnliftedArray\r\nimport GHC.Types\r\nimport GHC.Exts\r\n\r\nmain :: IO ()\r\nmain = do\r\n a@(Array myArr) < newArray 1 (\"foo\" :: String) >>= unsafeFreezeArray\r\n UnliftedArray myArrArr < newUnliftedArray 1 a >>= unsafeFreezeUnliftedArray\r\n putStrLn (myFunc show (2 :: Integer)) \r\n putStrLn (myFunc2 (\\x > show (Array x)) myArr) \r\n putStrLn (myBigFunc (+1) show show (2 :: Integer)) \r\n putStrLn (myBigFunc2 (\\x > array# (indexUnliftedArray (UnliftedArray x) 0 :: Array String)) (\\x > show (Array x)) (\\x > show (UnliftedArray x :: UnliftedArray (Array String))) myArrArr)\r\n\r\n{# NOINLINE myFunc #}\r\nmyFunc :: (a > String) > a > String\r\nmyFunc f a =\r\n let x = f a\r\n in x ++ x\r\n\r\nmyFunc2 :: forall (a :: TYPE 'UnliftedRep). (a > String) > a > String\r\nmyFunc2 = unsafeCoerce# myFunc\r\n\r\n{# NOINLINE myBigFunc #}\r\nmyBigFunc :: (a > b) > (b > String) > (a > String) > a > String\r\nmyBigFunc f g h a =\r\n let y = f a\r\n x = g y\r\n in x ++ x ++ h a\r\n\r\nmyBigFunc2 :: forall (a :: TYPE 'UnliftedRep) (b :: TYPE 'UnliftedRep). (a > b) > (b > String) > (a > String) > a > String\r\nmyBigFunc2 = unsafeCoerce# myBigFunc\r\n}}}\r\n\r\nThe compiles (surprisingly without a core lint error) and runs fine. So, here's the idea. We start with David's suggested change to `RuntimeRep`:\r\n\r\n{{{\r\ndata RuntimeRep\r\n = PtrRep Levity\r\n  ...\r\ndata Levity = Lifted  Unlifted\r\n}}}\r\n\r\nAnd then we change the check that disallows runtimerep polymorphism in binding positions to accept levity polymorphism in binding positions (but continuing to reject runtimerep polymorphism). For example, the two examples in the above code snippet would be rewritten as:\r\n\r\n{{{\r\n\r\nmyFunc :: forall (v :: Levity) (a :: TYPE ('PtrRep v)). (a > String) > a > String\r\nmyFunc = ...  same implementation\r\n\r\nmyBigFunc :: forall (v :: Levity) (w :: Levity) (a :: TYPE ('PtrRep v)) (b :: TYPE ('PtrRep w)). (a > b) > (b > String) > (a > String) > a > String\r\nmyBigFunc = ...  same implementation\r\n\r\n}}}\r\n\r\nAgain, GHC's runtime seems to already allow this. It's just the type system that's missing support for it. The only weird thing I can think of that comes up is that you cannot use bang patterns on a levitypolymorphic argument since unlifted values cannot be entered.\r\n\r\nI think it is possible to go a little further still. Fields of data types could be levity polymorphic:\r\n\r\n{{{\r\ndata List (a :: TYPE ('PtrRep v)) = Cons a (List a)  Nil\r\n\r\nmap :: forall (v :: Levity) (w :: Levity) (a :: TYPE ('PtrRep v)) (b :: TYPE ('PtrRep w)). (a > b) > List a > List b\r\n}}}\r\n\r\nAgain, bang patterns would need to be forbidden on such fields. This doesn't get us everything sought out in https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes, but it's kind of a halfway point that requires no changes to GHC's runtime and no changes to code generation. I think the whole thing can be handled in the type checker. Other potential application: `Array#` and `ArrayArray#` (and nearly all functions that operate on them) could be consolidated into a single type, reducing the number of duplicated primop implementations in GHC.\r\n\r\nOf course this would all need to be a GHC proposal, but I wanted to first solicit some feedback here on initial draft of the idea.","type_of_failure":"OtherFailure","blocking":[]} >I'm going to define two terms that I will use with these meanings for the remainder of this post.
1. RuntimeRep Polymorphism: full polymorphism in the runtime representation
1. Levity Polymorphism: polymorphism dealing with lifted vs unlifted types that are definitely represented by pointers.
GHC's levity polymorphism has the restriction that runtimereppolymorphic binders are not allowed. A comment David made recently on https://github.com/haskell/primitive/issues/198 got me thinking about the possibility of relaxing this restriction when it comes to dealing with a function with levitypolymorphic (not runtimereppolymorphic) binders. GHC's runtime already appears to allow doing this. AndrasKovacs writes on https://www.reddit.com/r/haskell/comments/6v9rmg/an_unified_array_interface/dlyug4e/ that he is able to store both lifted and unlifted values inside of the same `Array#` (pointing out as well that their primop implementations are identical) without crashing the GC. As further evidence that we can, roughly speaking, use lifted and unlifted values in the same places, I threw together a little experiment:
```
{# LANGUAGE MagicHash #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
import Data.Primitive
import Data.Primitive.UnliftedArray
import GHC.Types
import GHC.Exts
main :: IO ()
main = do
a@(Array myArr) < newArray 1 ("foo" :: String) >>= unsafeFreezeArray
UnliftedArray myArrArr < newUnliftedArray 1 a >>= unsafeFreezeUnliftedArray
putStrLn (myFunc show (2 :: Integer))
putStrLn (myFunc2 (\x > show (Array x)) myArr)
putStrLn (myBigFunc (+1) show show (2 :: Integer))
putStrLn (myBigFunc2 (\x > array# (indexUnliftedArray (UnliftedArray x) 0 :: Array String)) (\x > show (Array x)) (\x > show (UnliftedArray x :: UnliftedArray (Array String))) myArrArr)
{# NOINLINE myFunc #}
myFunc :: (a > String) > a > String
myFunc f a =
let x = f a
in x ++ x
myFunc2 :: forall (a :: TYPE 'UnliftedRep). (a > String) > a > String
myFunc2 = unsafeCoerce# myFunc
{# NOINLINE myBigFunc #}
myBigFunc :: (a > b) > (b > String) > (a > String) > a > String
myBigFunc f g h a =
let y = f a
x = g y
in x ++ x ++ h a
myBigFunc2 :: forall (a :: TYPE 'UnliftedRep) (b :: TYPE 'UnliftedRep). (a > b) > (b > String) > (a > String) > a > String
myBigFunc2 = unsafeCoerce# myBigFunc
```
The compiles (surprisingly without a core lint error) and runs fine. So, here's the idea. We start with David's suggested change to `RuntimeRep`:
```
data RuntimeRep
= PtrRep Levity
 ...
data Levity = Lifted  Unlifted
```
And then we change the check that disallows runtimerep polymorphism in binding positions to accept levity polymorphism in binding positions (but continuing to reject runtimerep polymorphism). For example, the two examples in the above code snippet would be rewritten as:
```
myFunc :: forall (v :: Levity) (a :: TYPE ('PtrRep v)). (a > String) > a > String
myFunc = ...  same implementation
myBigFunc :: forall (v :: Levity) (w :: Levity) (a :: TYPE ('PtrRep v)) (b :: TYPE ('PtrRep w)). (a > b) > (b > String) > (a > String) > a > String
myBigFunc = ...  same implementation
```
Again, GHC's runtime seems to already allow this. It's just the type system that's missing support for it. The only weird thing I can think of that comes up is that you cannot use bang patterns on a levitypolymorphic argument since unlifted values cannot be entered.
I think it is possible to go a little further still. Fields of data types could be levity polymorphic:
```
data List (a :: TYPE ('PtrRep v)) = Cons a (List a)  Nil
map :: forall (v :: Levity) (w :: Levity) (a :: TYPE ('PtrRep v)) (b :: TYPE ('PtrRep w)). (a > b) > List a > List b
```
Again, bang patterns would need to be forbidden on such fields. This doesn't get us everything sought out in https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes, but it's kind of a halfway point that requires no changes to GHC's runtime and no changes to code generation. I think the whole thing can be handled in the type checker. Other potential application: `Array#` and `ArrayArray#` (and nearly all functions that operate on them) could be consolidated into a single type, reducing the number of duplicated primop implementations in GHC.
Of course this would all need to be a GHC proposal, but I wanted to first solicit some feedback here on initial draft of the idea.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  dfeuer, goldfirere, simonpj, treeowl 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Relaxing LevityPolymorphic Binder Check for Lifted vs Unlifted pointers","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["LevityPolymorphism"],"differentials":[],"test_case":"","architecture":"","cc":["dfeuer","goldfirere","simonpj","treeowl"],"type":"FeatureRequest","description":"I'm going to define two terms that I will use with these meanings for the remainder of this post.\r\n\r\n1. RuntimeRep Polymorphism: full polymorphism in the runtime representation\r\n2. Levity Polymorphism: polymorphism dealing with lifted vs unlifted types that are definitely represented by pointers.\r\n\r\nGHC's levity polymorphism has the restriction that runtimereppolymorphic binders are not allowed. A comment David made recently on https://github.com/haskell/primitive/issues/198 got me thinking about the possibility of relaxing this restriction when it comes to dealing with a function with levitypolymorphic (not runtimereppolymorphic) binders. GHC's runtime already appears to allow doing this. AndrasKovacs writes on https://www.reddit.com/r/haskell/comments/6v9rmg/an_unified_array_interface/dlyug4e/ that he is able to store both lifted and unlifted values inside of the same `Array#` (pointing out as well that their primop implementations are identical) without crashing the GC. As further evidence that we can, roughly speaking, use lifted and unlifted values in the same places, I threw together a little experiment:\r\n\r\n{{{\r\n{# LANGUAGE MagicHash #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeInType #}\r\n\r\nimport Data.Primitive\r\nimport Data.Primitive.UnliftedArray\r\nimport GHC.Types\r\nimport GHC.Exts\r\n\r\nmain :: IO ()\r\nmain = do\r\n a@(Array myArr) < newArray 1 (\"foo\" :: String) >>= unsafeFreezeArray\r\n UnliftedArray myArrArr < newUnliftedArray 1 a >>= unsafeFreezeUnliftedArray\r\n putStrLn (myFunc show (2 :: Integer)) \r\n putStrLn (myFunc2 (\\x > show (Array x)) myArr) \r\n putStrLn (myBigFunc (+1) show show (2 :: Integer)) \r\n putStrLn (myBigFunc2 (\\x > array# (indexUnliftedArray (UnliftedArray x) 0 :: Array String)) (\\x > show (Array x)) (\\x > show (UnliftedArray x :: UnliftedArray (Array String))) myArrArr)\r\n\r\n{# NOINLINE myFunc #}\r\nmyFunc :: (a > String) > a > String\r\nmyFunc f a =\r\n let x = f a\r\n in x ++ x\r\n\r\nmyFunc2 :: forall (a :: TYPE 'UnliftedRep). (a > String) > a > String\r\nmyFunc2 = unsafeCoerce# myFunc\r\n\r\n{# NOINLINE myBigFunc #}\r\nmyBigFunc :: (a > b) > (b > String) > (a > String) > a > String\r\nmyBigFunc f g h a =\r\n let y = f a\r\n x = g y\r\n in x ++ x ++ h a\r\n\r\nmyBigFunc2 :: forall (a :: TYPE 'UnliftedRep) (b :: TYPE 'UnliftedRep). (a > b) > (b > String) > (a > String) > a > String\r\nmyBigFunc2 = unsafeCoerce# myBigFunc\r\n}}}\r\n\r\nThe compiles (surprisingly without a core lint error) and runs fine. So, here's the idea. We start with David's suggested change to `RuntimeRep`:\r\n\r\n{{{\r\ndata RuntimeRep\r\n = PtrRep Levity\r\n  ...\r\ndata Levity = Lifted  Unlifted\r\n}}}\r\n\r\nAnd then we change the check that disallows runtimerep polymorphism in binding positions to accept levity polymorphism in binding positions (but continuing to reject runtimerep polymorphism). For example, the two examples in the above code snippet would be rewritten as:\r\n\r\n{{{\r\n\r\nmyFunc :: forall (v :: Levity) (a :: TYPE ('PtrRep v)). (a > String) > a > String\r\nmyFunc = ...  same implementation\r\n\r\nmyBigFunc :: forall (v :: Levity) (w :: Levity) (a :: TYPE ('PtrRep v)) (b :: TYPE ('PtrRep w)). (a > b) > (b > String) > (a > String) > a > String\r\nmyBigFunc = ...  same implementation\r\n\r\n}}}\r\n\r\nAgain, GHC's runtime seems to already allow this. It's just the type system that's missing support for it. The only weird thing I can think of that comes up is that you cannot use bang patterns on a levitypolymorphic argument since unlifted values cannot be entered.\r\n\r\nI think it is possible to go a little further still. Fields of data types could be levity polymorphic:\r\n\r\n{{{\r\ndata List (a :: TYPE ('PtrRep v)) = Cons a (List a)  Nil\r\n\r\nmap :: forall (v :: Levity) (w :: Levity) (a :: TYPE ('PtrRep v)) (b :: TYPE ('PtrRep w)). (a > b) > List a > List b\r\n}}}\r\n\r\nAgain, bang patterns would need to be forbidden on such fields. This doesn't get us everything sought out in https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes, but it's kind of a halfway point that requires no changes to GHC's runtime and no changes to code generation. I think the whole thing can be handled in the type checker. Other potential application: `Array#` and `ArrayArray#` (and nearly all functions that operate on them) could be consolidated into a single type, reducing the number of duplicated primop implementations in GHC.\r\n\r\nOf course this would all need to be a GHC proposal, but I wanted to first solicit some feedback here on initial draft of the idea.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/17846runtimeRepPrimRep panic when combining UnboxedTuples with fhpc or {prof,fp...20200311T09:53:07ZRyan ScottruntimeRepPrimRep panic when combining UnboxedTuples with fhpc or {prof,fprofauto}(Originally observed in !2703.)
The following program:
```hs
{# LANGUAGE UnboxedTuples #}
module Bug where
makeUTup2 = (#,#)
```
Panics on GHC 8.0.2 or later if you compile it with `fhpc`:
```
$ /opt/ghc/8.8.2/bin/ghc fhpc fforcerecomp Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.2 for x86_64unknownlinux):
runtimeRepPrimRep
typePrimRep (a_12 :: TYPE k0_10)
k0_10
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/simplStg/RepType.hs:365:5 in ghc:RepType
```
Or, alternatively, with the combination of `prof` and `fprofauto`:
```
$ /opt/ghc/8.8.2/bin/ghc prof fprofauto fforcerecomp Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.2 for x86_64unknownlinux):
runtimeRepPrimRep
typePrimRep (a_12 :: TYPE k0_10)
k0_10
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/simplStg/RepType.hs:365:5 in ghc:RepType
```
A workaround is to manually etaexpand `mkUTup2`:
```hs
{# LANGUAGE UnboxedTuples #}
module Bug where
makeUTup2 x y = (# x, y #)
```(Originally observed in !2703.)
The following program:
```hs
{# LANGUAGE UnboxedTuples #}
module Bug where
makeUTup2 = (#,#)
```
Panics on GHC 8.0.2 or later if you compile it with `fhpc`:
```
$ /opt/ghc/8.8.2/bin/ghc fhpc fforcerecomp Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.2 for x86_64unknownlinux):
runtimeRepPrimRep
typePrimRep (a_12 :: TYPE k0_10)
k0_10
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/simplStg/RepType.hs:365:5 in ghc:RepType
```
Or, alternatively, with the combination of `prof` and `fprofauto`:
```
$ /opt/ghc/8.8.2/bin/ghc prof fprofauto fforcerecomp Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.2 for x86_64unknownlinux):
runtimeRepPrimRep
typePrimRep (a_12 :: TYPE k0_10)
k0_10
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
pprPanic, called at compiler/simplStg/RepType.hs:365:5 in ghc:RepType
```
A workaround is to manually etaexpand `mkUTup2`:
```hs
{# LANGUAGE UnboxedTuples #}
module Bug where
makeUTup2 x y = (# x, y #)
```https://gitlab.haskell.org/ghc/ghc//issues/17907Some levity polymorphism checks do not have coverage20200309T21:19:31ZKrzysztof GogolewskiSome levity polymorphism checks do not have coverageIf I remove several levity polymorphism checks:
https://gitlab.haskell.org/ghc/ghc/commit/25062762fd8d41230668cf90014f12a7c8199511
then GHC successfully validates. Either this code is no longer necessary, or we're missing some tests.If I remove several levity polymorphism checks:
https://gitlab.haskell.org/ghc/ghc/commit/25062762fd8d41230668cf90014f12a7c8199511
then GHC successfully validates. Either this code is no longer necessary, or we're missing some tests.https://gitlab.haskell.org/ghc/ghc//issues/17178Levity Polymorphic Pattern Synonyms20200217T14:51:54ZAndrew MartinLevity Polymorphic Pattern SynonymsGHC currently rejects the following program:
pattern Just# :: forall (r :: RuntimeRep) (a :: TYPE r). a > (# (# #)  a #)
pattern Just# a = (#  a #)
With this error message (the line number reference is the one where the signature of the pattern synonym is given):
A levitypolymorphic type is not allowed here:
Type: a
Kind: TYPE r

26  pattern Just# :: forall (r :: RuntimeRep) (a :: TYPE r). a > (# (# #)  a #)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
I would like for GHC to accept this pattern synonym. I think that it should just be possible to remove the levitypolymorphism check from pattern synonym signatures. I don't this can lead to any unsoundness since patterns are just expanded in Core.GHC currently rejects the following program:
pattern Just# :: forall (r :: RuntimeRep) (a :: TYPE r). a > (# (# #)  a #)
pattern Just# a = (#  a #)
With this error message (the line number reference is the one where the signature of the pattern synonym is given):
A levitypolymorphic type is not allowed here:
Type: a
Kind: TYPE r

26  pattern Just# :: forall (r :: RuntimeRep) (a :: TYPE r). a > (# (# #)  a #)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
I would like for GHC to accept this pattern synonym. I think that it should just be possible to remove the levitypolymorphism check from pattern synonym signatures. I don't this can lead to any unsoundness since patterns are just expanded in Core.https://gitlab.haskell.org/ghc/ghc//issues/17817Assertion failure with levity polymorphism20200217T14:48:18ZKrzysztof GogolewskiAssertion failure with levity polymorphismThe following code, taken from T13233, triggers an assertion failure in HEAD.
```haskell
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE UnboxedTuples #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE MagicHash #}
module Bug where
import GHC.Exts (TYPE, RuntimeRep, Weak#, State#, RealWorld, mkWeak# )
 It used to be that primops has no binding. However, as described in
 Note [Primop wrappers] in PrimOp we now rewrite unsaturated primop
 applications to their wrapper, which allows safe use of levity polymorphism.
primop :: forall (rep :: RuntimeRep) (a :: TYPE rep) b c.
a > b > (State# RealWorld > (# State# RealWorld, c #))
> State# RealWorld > (# State# RealWorld, Weak# b #)
primop = mkWeak#
```
```
WARNING: file compiler/coreSyn/CoreArity.hs, line 1122
4 forall (q :: RuntimeRep) (a :: TYPE q) b c.
a
> b
> (State# RealWorld > (# State# RealWorld, c #))
> State# RealWorld
> (# State# RealWorld, Weak# b #)
mkWeak#
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1248:29 in ghc:Outputable
warnPprTrace, called at compiler/coreSyn/CoreArity.hs:1122:11 in ghc:CoreArity
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.11.0.20200210:
ASSERT failed!
primop
Id arity: 4
STG arity: 0
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1187:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1257:5 in ghc:Outputable
assertPprPanic, called at compiler/GHC/CoreToStg.hs:314:66 in ghc:GHC.CoreToStg
```
This is not caught by the test itself, because it fails to compile due to other code present in this file. As a part of this ticket, let's split it into two (and remove `mkWeak#` from T13233_elab).The following code, taken from T13233, triggers an assertion failure in HEAD.
```haskell
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE UnboxedTuples #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE MagicHash #}
module Bug where
import GHC.Exts (TYPE, RuntimeRep, Weak#, State#, RealWorld, mkWeak# )
 It used to be that primops has no binding. However, as described in
 Note [Primop wrappers] in PrimOp we now rewrite unsaturated primop
 applications to their wrapper, which allows safe use of levity polymorphism.
primop :: forall (rep :: RuntimeRep) (a :: TYPE rep) b c.
a > b > (State# RealWorld > (# State# RealWorld, c #))
> State# RealWorld > (# State# RealWorld, Weak# b #)
primop = mkWeak#
```
```
WARNING: file compiler/coreSyn/CoreArity.hs, line 1122
4 forall (q :: RuntimeRep) (a :: TYPE q) b c.
a
> b
> (State# RealWorld > (# State# RealWorld, c #))
> State# RealWorld
> (# State# RealWorld, Weak# b #)
mkWeak#
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1248:29 in ghc:Outputable
warnPprTrace, called at compiler/coreSyn/CoreArity.hs:1122:11 in ghc:CoreArity
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.11.0.20200210:
ASSERT failed!
primop
Id arity: 4
STG arity: 0
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1187:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1257:5 in ghc:Outputable
assertPprPanic, called at compiler/GHC/CoreToStg.hs:314:66 in ghc:GHC.CoreToStg
```
This is not caught by the test itself, because it fails to compile due to other code present in this file. As a part of this ticket, let's split it into two (and remove `mkWeak#` from T13233_elab).https://gitlab.haskell.org/ghc/ghc//issues/17504Support unboxed types within Safe Haskell20191125T23:16:59ZKrzysztof GogolewskiSupport unboxed types within Safe HaskellCurrently, it is not possible to use unboxed types such as `Int#` or levity polymorphism (`RuntimeRep`, `TYPE`) with Safe Haskell, because `GHC.Prim` and `GHC.Types` are marked as unsafe.
As a first step, we could export `RuntimeRep` and `TYPE` from the module `Data.Kind`.
See also thread "Exposed # kinded variables + polykinded Prelude classes?" at the libraries mailing list, Oct 2019.Currently, it is not possible to use unboxed types such as `Int#` or levity polymorphism (`RuntimeRep`, `TYPE`) with Safe Haskell, because `GHC.Prim` and `GHC.Types` are marked as unsafe.
As a first step, we could export `RuntimeRep` and `TYPE` from the module `Data.Kind`.
See also thread "Exposed # kinded variables + polykinded Prelude classes?" at the libraries mailing list, Oct 2019.https://gitlab.haskell.org/ghc/ghc//issues/14917Allow levity polymorphism in binding position20191112T18:22:11ZAndrew MartinAllow levity polymorphism in binding positionThe main problem with levity polymorphism in a binding position is that it's impossible to do codegen since the calling convention depending on the instantiation of the runtime representation variable. From the paper, we have the following rejected example code:
```
bTwice :: ∀ (r :: RuntimeRep) (a :: TYPE r). Bool → a → (a → a) → a
```
However, if you are able to inline the function, this problem disappears. You would need a guarantee stronger than what the `INLINE` pragma provides though since the `INLINE` pragma still allows the function to be fed as an argument to a higherorder function. I'll refer to a hypothetical new pragma as `INLINE MANDATE`. This pragma causes a compiletime error to be admitted if the function is ever used in a way that would cause it to not be inlined. Now `bTwice` would be writeable:
```
{# INLINE MANDATE #}
bTwice :: ∀ (r :: RuntimeRep) (a :: TYPE r). Bool → a → (a → a) → a
```
The function definition would be provide in the `.hi` file just as it would be for a function marked as `INLINE`, but unlike the `INLINE` counterpart, there would be no generated code for this function, since generating the code would be impossible.
I have several uses for this in mind. I often want a levitypolymorphic variant `ST`. With `INLINE MANDATE`, I still wouldn't get `do` notation, but I could write:
```
 This newtype is already allowed today
newtype STL s (a :: TYPE r) = STL (State# s > (# s, a #) #)
intA, intB, intC :: STL s Int#
wordA, wordB :: Int# > STL s Word#
{# INLINE MANDATE #}
(>>=.) :: STL s a > (a > STL s b) > STL s b
STL a >>=. g = STL (\s0 > case a s0 of
(# s1, v #) > case g v of
STL f > f s1
myFunc :: STL s Word#
myFunc =
intA >>=. \a >
intB >>=. \b >
intC >>=. \c >
wordA a >>=. \wa >
wordB b >>=. \wb >
...  do something with the data
```
I would appreciate any feedback on this. If there's something that makes this fundamentally impossible, that would be good to know. Or if other people feel like this would be useful, that would be good to know as well.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Allow levity polymorhism in binding position","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["LevityPolymorphism"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"The main problem with levity polymorphism in a binding position is that it's impossible to do codegen since the calling convention depending on the instantiation of the runtime representation variable. From the paper, we have the following rejected example code:\r\n\r\n{{{\r\nbTwice :: ∀ (r :: RuntimeRep) (a :: TYPE r). Bool → a → (a → a) → a\r\n}}}\r\n\r\nHowever, if you are able to inline the function, this problem disappears. You would need a guarantee stronger than what the `INLINE` pragma provides though since the `INLINE` pragma still allows the function to be fed as an argument to a higherorder function. I'll refer to a hypothetical new pragma as `INLINE MANDATE`. This pragma causes a compiletime error to be admitted if the function is ever used in a way that would cause it to not be inlined. Now `bTwice` would be writeable:\r\n\r\n{{{\r\n{# INLINE MANDATE #}\r\nbTwice :: ∀ (r :: RuntimeRep) (a :: TYPE r). Bool → a → (a → a) → a\r\n}}}\r\n\r\nThe function definition would be provide in the `.hi` file just as it would be for a function marked as `INLINE`, but unlike the `INLINE` counterpart, there would be no generated code for this function, since generating the code would be impossible.\r\n\r\nI have several uses for this in mind. I often want a levitypolymorphic variant `ST`. With `INLINE MANDATE`, I still wouldn't get `do` notation, but I could write:\r\n\r\n{{{\r\n This newtype is already allowed today\r\nnewtype STL s (a :: TYPE r) = STL (State# s > (# s, a #) #)\r\n\r\nintA, intB, intC :: STL s Int#\r\nwordA, wordB :: Int# > STL s Word#\r\n\r\n{# INLINE MANDATE #}\r\n(>>=.) :: STL s a > (a > STL s b) > STL s b\r\nSTL a >>=. g = STL (\\s0 > case a s0 of\r\n (# s1, v #) > case g v of\r\n STL f > f s1\r\n\r\nmyFunc :: STL s Word#\r\nmyFunc =\r\n intA >>=. \\a >\r\n intB >>=. \\b > \r\n intC >>=. \\c > \r\n wordA a >>=. \\wa > \r\n wordB b >>=. \\wb >\r\n ...  do something with the data\r\n}}}\r\n\r\nI would appreciate any feedback on this. If there's something that makes this fundamentally impossible, that would be good to know. Or if other people feel like this would be useful, that would be good to know as well.","type_of_failure":"OtherFailure","blocking":[]} >The main problem with levity polymorphism in a binding position is that it's impossible to do codegen since the calling convention depending on the instantiation of the runtime representation variable. From the paper, we have the following rejected example code:
```
bTwice :: ∀ (r :: RuntimeRep) (a :: TYPE r). Bool → a → (a → a) → a
```
However, if you are able to inline the function, this problem disappears. You would need a guarantee stronger than what the `INLINE` pragma provides though since the `INLINE` pragma still allows the function to be fed as an argument to a higherorder function. I'll refer to a hypothetical new pragma as `INLINE MANDATE`. This pragma causes a compiletime error to be admitted if the function is ever used in a way that would cause it to not be inlined. Now `bTwice` would be writeable:
```
{# INLINE MANDATE #}
bTwice :: ∀ (r :: RuntimeRep) (a :: TYPE r). Bool → a → (a → a) → a
```
The function definition would be provide in the `.hi` file just as it would be for a function marked as `INLINE`, but unlike the `INLINE` counterpart, there would be no generated code for this function, since generating the code would be impossible.
I have several uses for this in mind. I often want a levitypolymorphic variant `ST`. With `INLINE MANDATE`, I still wouldn't get `do` notation, but I could write:
```
 This newtype is already allowed today
newtype STL s (a :: TYPE r) = STL (State# s > (# s, a #) #)
intA, intB, intC :: STL s Int#
wordA, wordB :: Int# > STL s Word#
{# INLINE MANDATE #}
(>>=.) :: STL s a > (a > STL s b) > STL s b
STL a >>=. g = STL (\s0 > case a s0 of
(# s1, v #) > case g v of
STL f > f s1
myFunc :: STL s Word#
myFunc =
intA >>=. \a >
intB >>=. \b >
intC >>=. \c >
wordA a >>=. \wa >
wordB b >>=. \wb >
...  do something with the data
```
I would appreciate any feedback on this. If there's something that makes this fundamentally impossible, that would be good to know. Or if other people feel like this would be useful, that would be good to know as well.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Allow levity polymorhism in binding position","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["LevityPolymorphism"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"The main problem with levity polymorphism in a binding position is that it's impossible to do codegen since the calling convention depending on the instantiation of the runtime representation variable. From the paper, we have the following rejected example code:\r\n\r\n{{{\r\nbTwice :: ∀ (r :: RuntimeRep) (a :: TYPE r). Bool → a → (a → a) → a\r\n}}}\r\n\r\nHowever, if you are able to inline the function, this problem disappears. You would need a guarantee stronger than what the `INLINE` pragma provides though since the `INLINE` pragma still allows the function to be fed as an argument to a higherorder function. I'll refer to a hypothetical new pragma as `INLINE MANDATE`. This pragma causes a compiletime error to be admitted if the function is ever used in a way that would cause it to not be inlined. Now `bTwice` would be writeable:\r\n\r\n{{{\r\n{# INLINE MANDATE #}\r\nbTwice :: ∀ (r :: RuntimeRep) (a :: TYPE r). Bool → a → (a → a) → a\r\n}}}\r\n\r\nThe function definition would be provide in the `.hi` file just as it would be for a function marked as `INLINE`, but unlike the `INLINE` counterpart, there would be no generated code for this function, since generating the code would be impossible.\r\n\r\nI have several uses for this in mind. I often want a levitypolymorphic variant `ST`. With `INLINE MANDATE`, I still wouldn't get `do` notation, but I could write:\r\n\r\n{{{\r\n This newtype is already allowed today\r\nnewtype STL s (a :: TYPE r) = STL (State# s > (# s, a #) #)\r\n\r\nintA, intB, intC :: STL s Int#\r\nwordA, wordB :: Int# > STL s Word#\r\n\r\n{# INLINE MANDATE #}\r\n(>>=.) :: STL s a > (a > STL s b) > STL s b\r\nSTL a >>=. g = STL (\\s0 > case a s0 of\r\n (# s1, v #) > case g v of\r\n STL f > f s1\r\n\r\nmyFunc :: STL s Word#\r\nmyFunc =\r\n intA >>=. \\a >\r\n intB >>=. \\b > \r\n intC >>=. \\c > \r\n wordA a >>=. \\wa > \r\n wordB b >>=. \\wb >\r\n ...  do something with the data\r\n}}}\r\n\r\nI would appreciate any feedback on this. If there's something that makes this fundamentally impossible, that would be good to know. Or if other people feel like this would be useful, that would be good to know as well.","type_of_failure":"OtherFailure","blocking":[]} >John EricsonJohn Ericsonhttps://gitlab.haskell.org/ghc/ghc//issues/16964Documentation of RuntimeRep is wrong about 64bit integer reps20191101T12:00:29ZÖmer Sinan AğacanDocumentation of RuntimeRep is wrong about 64bit integer repsDocumentation of `Int64Rep` and `Word64Rep` currently have the note "on 32bit only" which seems wrong. Here's an example (this is on a 64bit system):
```
~ $ cat Main.hs
{# LANGUAGE TypeApplications, MagicHash #}
import Type.Reflection
import GHC.Types
import GHC.Prim
import Data.Int
main = do
print (splitApps (typeRepKind (typeRep @Int64#)))
print (splitApps (typeRepKind (typeRep @Int#)))
~ $ ghc Main.hs
[1 of 1] Compiling Main ( Main.hs, Main.o )
Linking Main ...
~ $ ./Main
(TYPE,['Int64Rep])
(TYPE,['IntRep])
```
The documentation seems to suggest that `Int64Rep` should only be used on 32bit systems, and we should get `IntRep` for `Int64#` on 64bit.
[(Link to `RuntimeRep`)](https://hackage.haskell.org/package/base4.12.0.0/docs/GHCExts.html#t:RuntimeRep)
(The same comments exist in GHC HEAD source tree too)
(cc @rae)Documentation of `Int64Rep` and `Word64Rep` currently have the note "on 32bit only" which seems wrong. Here's an example (this is on a 64bit system):
```
~ $ cat Main.hs
{# LANGUAGE TypeApplications, MagicHash #}
import Type.Reflection
import GHC.Types
import GHC.Prim
import Data.Int
main = do
print (splitApps (typeRepKind (typeRep @Int64#)))
print (splitApps (typeRepKind (typeRep @Int#)))
~ $ ghc Main.hs
[1 of 1] Compiling Main ( Main.hs, Main.o )
Linking Main ...
~ $ ./Main
(TYPE,['Int64Rep])
(TYPE,['IntRep])
```
The documentation seems to suggest that `Int64Rep` should only be used on 32bit systems, and we should get `IntRep` for `Int64#` on 64bit.
[(Link to `RuntimeRep`)](https://hackage.haskell.org/package/base4.12.0.0/docs/GHCExts.html#t:RuntimeRep)
(The same comments exist in GHC HEAD source tree too)
(cc @rae)8.8.1John EricsonCarter SchonwaldJohn Ericsonhttps://gitlab.haskell.org/ghc/ghc//issues/17268Arcane interaction of RuntimeRep with StandaloneKindSignatures20191008T17:16:17ZVladislav ZavialovArcane interaction of RuntimeRep with StandaloneKindSignaturesConsider this program:
```
{# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, StandaloneKindSignatures #}
import Data.Kind
data R
type TY :: R > Type
data TY r
data A (a :: TY r) = MkA (B a)
data B a = MkB (A a)
```
We can discover the inferred kind of `A` in GHCi:
```
ghci> :k A
A :: forall (r :: R). TY r > Type
```
And then, sure enough, we can copy this signature into the original program:
```
{# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, StandaloneKindSignatures #}
import Data.Kind
data R
type TY :: R > Type
data TY r
type A :: forall (r :: R). TY r > Type
data A (a :: TY r) = MkA (B a)
data B a = MkB (A a)
```
This compiles fine. Now, let's repeat the experiment using `RuntimeRep` instead of a new data type `R`:
```
{# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, StandaloneKindSignatures #}
import Data.Kind
import GHC.Exts
type R = RuntimeRep
type TY :: R > Type
data TY r
data A (a :: TY r) = MkA (B a)
data B a = MkB (A a)
```
To check the kind of `A` in GHCi, let's not forget `fprintexplicitruntimereps`:
```
ghci> :set fprintexplicitruntimereps
ghci> :k A
A :: forall (r :: R). TY r > Type
```
This time, if we paste this signature into the original program, we get a kind error:
```
{# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, StandaloneKindSignatures #}
import Data.Kind
import GHC.Exts
type R = RuntimeRep
type TY :: R > Type
data TY r
type A :: forall (r :: R). TY r > Type
data A (a :: TY r) = MkA (B a)
data B a = MkB (A a)
```
```
Test.hs:12:29: error:
• Expected kind ‘TY 'LiftedRep’, but ‘a’ has kind ‘TY r’
• In the first argument of ‘B’, namely ‘a’
In the type ‘(B a)’
In the definition of data constructor ‘MkA’

12  data A (a :: TY r) = MkA (B a)

```
How come?Consider this program:
```
{# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, StandaloneKindSignatures #}
import Data.Kind
data R
type TY :: R > Type
data TY r
data A (a :: TY r) = MkA (B a)
data B a = MkB (A a)
```
We can discover the inferred kind of `A` in GHCi:
```
ghci> :k A
A :: forall (r :: R). TY r > Type
```
And then, sure enough, we can copy this signature into the original program:
```
{# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, StandaloneKindSignatures #}
import Data.Kind
data R
type TY :: R > Type
data TY r
type A :: forall (r :: R). TY r > Type
data A (a :: TY r) = MkA (B a)
data B a = MkB (A a)
```
This compiles fine. Now, let's repeat the experiment using `RuntimeRep` instead of a new data type `R`:
```
{# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, StandaloneKindSignatures #}
import Data.Kind
import GHC.Exts
type R = RuntimeRep
type TY :: R > Type
data TY r
data A (a :: TY r) = MkA (B a)
data B a = MkB (A a)
```
To check the kind of `A` in GHCi, let's not forget `fprintexplicitruntimereps`:
```
ghci> :set fprintexplicitruntimereps
ghci> :k A
A :: forall (r :: R). TY r > Type
```
This time, if we paste this signature into the original program, we get a kind error:
```
{# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, StandaloneKindSignatures #}
import Data.Kind
import GHC.Exts
type R = RuntimeRep
type TY :: R > Type
data TY r
type A :: forall (r :: R). TY r > Type
data A (a :: TY r) = MkA (B a)
data B a = MkB (A a)
```
```
Test.hs:12:29: error:
• Expected kind ‘TY 'LiftedRep’, but ‘a’ has kind ‘TY r’
• In the first argument of ‘B’, namely ‘a’
In the type ‘(B a)’
In the definition of data constructor ‘MkA’

12  data A (a :: TY r) = MkA (B a)

```
How come?https://gitlab.haskell.org/ghc/ghc//issues/14185Nonlocal bug reporting around levity polymorphism20190707T18:18:03ZRichard Eisenbergrae@richarde.devNonlocal bug reporting around levity polymorphismFrom [ticket:13105\#comment:141886](https://gitlab.haskell.org//ghc/ghc/issues/13105#note_141886).
In HEAD (or, at least, my version, on the `wip/rae` branch), this code
```hs
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)
testInt :: Int
testInt = box (unbox 1)
testTup :: (Int, Char)
testTup = box (unbox (1, 'a'))
```
fails with
```
Bug.hs:27:11: error:
• Couldn't match a lifted type with an unlifted type
When matching types
a' :: *
Int# :: TYPE 'IntRep
• In the expression: box (unbox 1)
In an equation for ‘testInt’: testInt = box (unbox 1)

27  testInt = box (unbox 1)
 ^^^^^^^^^^^^^
Bug.hs:27:16: error:
• Couldn't match a lifted type with an unlifted type
When matching types
a' :: *
Int# :: TYPE 'IntRep
• In the first argument of ‘box’, namely ‘(unbox 1)’
In the expression: box (unbox 1)
In an equation for ‘testInt’: testInt = box (unbox 1)

27  testInt = box (unbox 1)
 ^^^^^^^
Bug.hs:42:11: error:
• Couldn't match a lifted type with an unlifted type
When matching types
a' :: *
Int# :: TYPE 'IntRep
• In the expression: box (unbox (1, 'a'))
In an equation for ‘testTup’: testTup = box (unbox (1, 'a'))

42  testTup = box (unbox (1, 'a'))
 ^^^^^^^^^^^^^^^^^^^^
```
I think it should succeed. Worse, when I comment out the `testTup` definition, the file succeeds... but note that two of the errors above are in `testInt`, which compiles fine on its own.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Nonlocal bug reporting around levity polymorphism","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["LevityPolymorphism,","TypeErrorMessages"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"From comment:12:ticket:13105.\r\n\r\nIn HEAD (or, at least, my version, on the `wip/rae` branch), this code\r\n\r\n{{{#!hs\r\nclass Unbox (t :: *) (r :: TYPE k)  t > r, r > t where\r\n unbox :: t > r\r\n box :: r > t\r\n \r\ninstance Unbox Int Int# where\r\n unbox (I# i) = i\r\n box i = I# i\r\n\r\ninstance Unbox Char Char# where\r\n unbox (C# c) = c\r\n box c = C# c\r\n\r\ninstance (Unbox a a', Unbox b b') => Unbox (a,b) (# a', b' #) where\r\n unbox (a,b) = (# unbox a, unbox b #)\r\n box (# a, b #) = (box a, box b)\r\n\r\ntestInt :: Int\r\ntestInt = box (unbox 1)\r\n\r\ntestTup :: (Int, Char)\r\ntestTup = box (unbox (1, 'a'))\r\n}}}\r\n\r\nfails with\r\n\r\n{{{\r\nBug.hs:27:11: error:\r\n • Couldn't match a lifted type with an unlifted type\r\n When matching types\r\n a' :: *\r\n Int# :: TYPE 'IntRep\r\n • In the expression: box (unbox 1)\r\n In an equation for ‘testInt’: testInt = box (unbox 1)\r\n \r\n27  testInt = box (unbox 1)\r\n  ^^^^^^^^^^^^^\r\n\r\nBug.hs:27:16: error:\r\n • Couldn't match a lifted type with an unlifted type\r\n When matching types\r\n a' :: *\r\n Int# :: TYPE 'IntRep\r\n • In the first argument of ‘box’, namely ‘(unbox 1)’\r\n In the expression: box (unbox 1)\r\n In an equation for ‘testInt’: testInt = box (unbox 1)\r\n \r\n27  testInt = box (unbox 1)\r\n  ^^^^^^^\r\n\r\nBug.hs:42:11: error:\r\n • Couldn't match a lifted type with an unlifted type\r\n When matching types\r\n a' :: *\r\n Int# :: TYPE 'IntRep\r\n • In the expression: box (unbox (1, 'a'))\r\n In an equation for ‘testTup’: testTup = box (unbox (1, 'a'))\r\n \r\n42  testTup = box (unbox (1, 'a'))\r\n  ^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nI think it should succeed. Worse, when I comment out the `testTup` definition, the file succeeds... but note that two of the errors above are in `testInt`, which compiles fine on its own.","type_of_failure":"OtherFailure","blocking":[]} >From [ticket:13105\#comment:141886](https://gitlab.haskell.org//ghc/ghc/issues/13105#note_141886).
In HEAD (or, at least, my version, on the `wip/rae` branch), this code
```hs
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)
testInt :: Int
testInt = box (unbox 1)
testTup :: (Int, Char)
testTup = box (unbox (1, 'a'))
```
fails with
```
Bug.hs:27:11: error:
• Couldn't match a lifted type with an unlifted type
When matching types
a' :: *
Int# :: TYPE 'IntRep
• In the expression: box (unbox 1)
In an equation for ‘testInt’: testInt = box (unbox 1)

27  testInt = box (unbox 1)
 ^^^^^^^^^^^^^
Bug.hs:27:16: error:
• Couldn't match a lifted type with an unlifted type
When matching types
a' :: *
Int# :: TYPE 'IntRep
• In the first argument of ‘box’, namely ‘(unbox 1)’
In the expression: box (unbox 1)
In an equation for ‘testInt’: testInt = box (unbox 1)

27  testInt = box (unbox 1)
 ^^^^^^^
Bug.hs:42:11: error:
• Couldn't match a lifted type with an unlifted type
When matching types
a' :: *
Int# :: TYPE 'IntRep
• In the expression: box (unbox (1, 'a'))
In an equation for ‘testTup’: testTup = box (unbox (1, 'a'))

42  testTup = box (unbox (1, 'a'))
 ^^^^^^^^^^^^^^^^^^^^
```
I think it should succeed. Worse, when I comment out the `testTup` definition, the file succeeds... but note that two of the errors above are in `testInt`, which compiles fine on its own.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Nonlocal bug reporting around levity polymorphism","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["LevityPolymorphism,","TypeErrorMessages"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"From comment:12:ticket:13105.\r\n\r\nIn HEAD (or, at least, my version, on the `wip/rae` branch), this code\r\n\r\n{{{#!hs\r\nclass Unbox (t :: *) (r :: TYPE k)  t > r, r > t where\r\n unbox :: t > r\r\n box :: r > t\r\n \r\ninstance Unbox Int Int# where\r\n unbox (I# i) = i\r\n box i = I# i\r\n\r\ninstance Unbox Char Char# where\r\n unbox (C# c) = c\r\n box c = C# c\r\n\r\ninstance (Unbox a a', Unbox b b') => Unbox (a,b) (# a', b' #) where\r\n unbox (a,b) = (# unbox a, unbox b #)\r\n box (# a, b #) = (box a, box b)\r\n\r\ntestInt :: Int\r\ntestInt = box (unbox 1)\r\n\r\ntestTup :: (Int, Char)\r\ntestTup = box (unbox (1, 'a'))\r\n}}}\r\n\r\nfails with\r\n\r\n{{{\r\nBug.hs:27:11: error:\r\n • Couldn't match a lifted type with an unlifted type\r\n When matching types\r\n a' :: *\r\n Int# :: TYPE 'IntRep\r\n • In the expression: box (unbox 1)\r\n In an equation for ‘testInt’: testInt = box (unbox 1)\r\n \r\n27  testInt = box (unbox 1)\r\n  ^^^^^^^^^^^^^\r\n\r\nBug.hs:27:16: error:\r\n • Couldn't match a lifted type with an unlifted type\r\n When matching types\r\n a' :: *\r\n Int# :: TYPE 'IntRep\r\n • In the first argument of ‘box’, namely ‘(unbox 1)’\r\n In the expression: box (unbox 1)\r\n In an equation for ‘testInt’: testInt = box (unbox 1)\r\n \r\n27  testInt = box (unbox 1)\r\n  ^^^^^^^\r\n\r\nBug.hs:42:11: error:\r\n • Couldn't match a lifted type with an unlifted type\r\n When matching types\r\n a' :: *\r\n Int# :: TYPE 'IntRep\r\n • In the expression: box (unbox (1, 'a'))\r\n In an equation for ‘testTup’: testTup = box (unbox (1, 'a'))\r\n \r\n42  testTup = box (unbox (1, 'a'))\r\n  ^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nI think it should succeed. Worse, when I comment out the `testTup` definition, the file succeeds... but note that two of the errors above are in `testInt`, which compiles fine on its own.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14196Replace ArrayArray# with either UnliftedArray# or Array#20190707T18:18:00ZAndrew MartinReplace ArrayArray# with either UnliftedArray# or Array#Just to be clear, there currently is nothing named `UnliftedArray#`. I would like to propose that such a thing possibly be added, with the longterm goal of deprecating and removing `ArrayArray#`. The interface for it would look like this:
```hs
data UnliftedArray# (a :: TYPE 'UnliftedRep)
data MutableUnliftedArray# s (a :: TYPE 'UnliftedRep)
indexUnliftedArray# :: forall (a :: TYPE 'UnliftedRep). UnliftedArray# a > Int# > a
writeUnliftedArray# :: forall (a :: TYPE 'UnliftedRep). MutableUnliftedArray# s a > Int# > a > State# s > State# s
readUnliftedArray# :: forall (a :: TYPE 'UnliftedRep). MutableUnliftedArray# s a > Int# > State# s > (# State# s, a #)
unsafeFreezeUnliftedArray# :: forall (a :: TYPE 'UnliftedRep). MutableUnliftedArray# s a > State# s > (#State# s, UnliftedArray# a#)
newUnliftedArray# :: forall (a :: TYPE 'UnliftedRep). Int# > a > State# s > (# State# s, MutableUnliftedArray# s a #)
```
You would also have a few other things like `sameMutableUnliftedArray#`, `sizeofMutableArray#`, `unsafeThawUnliftedArray#`, `copyUnliftedArray#`, etc. The main difficulty that I see in doing this is that I'm not sure if you can tell a primop that it takes a polymorphic argument whose kind is something other than `TYPE LiftedRep`. The bodies of all of the functions I listed above could simply be copied from the `ArrayArray#` functions.
There are a few alternatives I've heard discussed. One is to make `Array#` accepted both boxed or unboxed types. There is a brief discussion of this in the UnliftedDataTypes proposal \[\#point0 (0)\]. Indeed, it appears that some have managed to smuggle unlifted data into `Array#` already, with the caveats one would expect \[\#point1 (1)\]. This interface would look like:
```hs
data Array# (a :: TYPE k)
data MutableArray# s (a :: TYPE k)
indexArray# :: Array# a > Int > a  same as before
indexUnliftedArray# :: forall (a :: TYPE UnliftedRep). Array# a > Int > a
```
So instead of having `Array#` and `UnliftedArray#` as separate data types, we could have `Array#` handle both cases, but we would need to make a duplicate of every function that operates on `Array#`. This follows all of the appropriate rules for when levity polymorphism is allowed, and it should be backwardscompatible with the previous nonlevitypolymorphic definition of `Array#`. I'm not sure how many things in the GHC runtime assume that the values inside an array are lifted, so this might cause a bunch of problems. If it is possible, this approach would be kind of neat because then `SmallArray#` could be similarly adapted.
Anyway, I just wanted to get this out there. I would be happy to try implementing the first proposal (involving `UnliftedArray#`) at some point in the next six months. Any feedback on the idea would be appreciated. Also, any comments on how appropriate this is for someone new to contributing to GHC would be appreciated as well. Thanks.
 \[=\#point0 (0)\] https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes\#Parametricity
 \[=\#point0 (1)\] https://www.reddit.com/r/haskell/comments/6v9rmg/an_unified_array_interface/dlyph4i/
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Replace ArrayArray# with either UnliftedArray# or Array#","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["LevityPolymorphism"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Just to be clear, there currently is nothing named `UnliftedArray#`. I would like to propose that such a thing possibly be added, with the longterm goal of deprecating and removing `ArrayArray#`. The interface for it would look like this:\r\n\r\n{{{#!hs\r\ndata UnliftedArray# (a :: TYPE 'UnliftedRep)\r\ndata MutableUnliftedArray# s (a :: TYPE 'UnliftedRep)\r\n\r\nindexUnliftedArray# :: forall (a :: TYPE 'UnliftedRep). UnliftedArray# a > Int# > a\r\nwriteUnliftedArray# :: forall (a :: TYPE 'UnliftedRep). MutableUnliftedArray# s a > Int# > a > State# s > State# s\r\nreadUnliftedArray# :: forall (a :: TYPE 'UnliftedRep). MutableUnliftedArray# s a > Int# > State# s > (# State# s, a #)\r\nunsafeFreezeUnliftedArray# :: forall (a :: TYPE 'UnliftedRep). MutableUnliftedArray# s a > State# s > (#State# s, UnliftedArray# a#)\r\nnewUnliftedArray# :: forall (a :: TYPE 'UnliftedRep). Int# > a > State# s > (# State# s, MutableUnliftedArray# s a #)\r\n}}}\r\n\r\nYou would also have a few other things like `sameMutableUnliftedArray#`, `sizeofMutableArray#`, `unsafeThawUnliftedArray#`, `copyUnliftedArray#`, etc. The main difficulty that I see in doing this is that I'm not sure if you can tell a primop that it takes a polymorphic argument whose kind is something other than `TYPE LiftedRep`. The bodies of all of the functions I listed above could simply be copied from the `ArrayArray#` functions.\r\n\r\nThere are a few alternatives I've heard discussed. One is to make `Array#` accepted both boxed or unboxed types. There is a brief discussion of this in the UnliftedDataTypes proposal [#point0 (0)]. Indeed, it appears that some have managed to smuggle unlifted data into `Array#` already, with the caveats one would expect [#point1 (1)]. This interface would look like:\r\n\r\n{{{#!hs\r\ndata Array# (a :: TYPE k)\r\ndata MutableArray# s (a :: TYPE k)\r\nindexArray# :: Array# a > Int > a  same as before\r\nindexUnliftedArray# :: forall (a :: TYPE UnliftedRep). Array# a > Int > a\r\n}}}\r\n\r\nSo instead of having `Array#` and `UnliftedArray#` as separate data types, we could have `Array#` handle both cases, but we would need to make a duplicate of every function that operates on `Array#`. This follows all of the appropriate rules for when levity polymorphism is allowed, and it should be backwardscompatible with the previous nonlevitypolymorphic definition of `Array#`. I'm not sure how many things in the GHC runtime assume that the values inside an array are lifted, so this might cause a bunch of problems. If it is possible, this approach would be kind of neat because then `SmallArray#` could be similarly adapted.\r\n\r\nAnyway, I just wanted to get this out there. I would be happy to try implementing the first proposal (involving `UnliftedArray#`) at some point in the next six months. Any feedback on the idea would be appreciated. Also, any comments on how appropriate this is for someone new to contributing to GHC would be appreciated as well. Thanks.\r\n\r\n* [=#point0 (0)] https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes#Parametricity\r\n* [=#point0 (1)] https://www.reddit.com/r/haskell/comments/6v9rmg/an_unified_array_interface/dlyph4i/","type_of_failure":"OtherFailure","blocking":[]} >Just to be clear, there currently is nothing named `UnliftedArray#`. I would like to propose that such a thing possibly be added, with the longterm goal of deprecating and removing `ArrayArray#`. The interface for it would look like this:
```hs
data UnliftedArray# (a :: TYPE 'UnliftedRep)
data MutableUnliftedArray# s (a :: TYPE 'UnliftedRep)
indexUnliftedArray# :: forall (a :: TYPE 'UnliftedRep). UnliftedArray# a > Int# > a
writeUnliftedArray# :: forall (a :: TYPE 'UnliftedRep). MutableUnliftedArray# s a > Int# > a > State# s > State# s
readUnliftedArray# :: forall (a :: TYPE 'UnliftedRep). MutableUnliftedArray# s a > Int# > State# s > (# State# s, a #)
unsafeFreezeUnliftedArray# :: forall (a :: TYPE 'UnliftedRep). MutableUnliftedArray# s a > State# s > (#State# s, UnliftedArray# a#)
newUnliftedArray# :: forall (a :: TYPE 'UnliftedRep). Int# > a > State# s > (# State# s, MutableUnliftedArray# s a #)
```
You would also have a few other things like `sameMutableUnliftedArray#`, `sizeofMutableArray#`, `unsafeThawUnliftedArray#`, `copyUnliftedArray#`, etc. The main difficulty that I see in doing this is that I'm not sure if you can tell a primop that it takes a polymorphic argument whose kind is something other than `TYPE LiftedRep`. The bodies of all of the functions I listed above could simply be copied from the `ArrayArray#` functions.
There are a few alternatives I've heard discussed. One is to make `Array#` accepted both boxed or unboxed types. There is a brief discussion of this in the UnliftedDataTypes proposal \[\#point0 (0)\]. Indeed, it appears that some have managed to smuggle unlifted data into `Array#` already, with the caveats one would expect \[\#point1 (1)\]. This interface would look like:
```hs
data Array# (a :: TYPE k)
data MutableArray# s (a :: TYPE k)
indexArray# :: Array# a > Int > a  same as before
indexUnliftedArray# :: forall (a :: TYPE UnliftedRep). Array# a > Int > a
```
So instead of having `Array#` and `UnliftedArray#` as separate data types, we could have `Array#` handle both cases, but we would need to make a duplicate of every function that operates on `Array#`. This follows all of the appropriate rules for when levity polymorphism is allowed, and it should be backwardscompatible with the previous nonlevitypolymorphic definition of `Array#`. I'm not sure how many things in the GHC runtime assume that the values inside an array are lifted, so this might cause a bunch of problems. If it is possible, this approach would be kind of neat because then `SmallArray#` could be similarly adapted.
Anyway, I just wanted to get this out there. I would be happy to try implementing the first proposal (involving `UnliftedArray#`) at some point in the next six months. Any feedback on the idea would be appreciated. Also, any comments on how appropriate this is for someone new to contributing to GHC would be appreciated as well. Thanks.
 \[=\#point0 (0)\] https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes\#Parametricity
 \[=\#point0 (1)\] https://www.reddit.com/r/haskell/comments/6v9rmg/an_unified_array_interface/dlyph4i/
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Replace ArrayArray# with either UnliftedArray# or Array#","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["LevityPolymorphism"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Just to be clear, there currently is nothing named `UnliftedArray#`. I would like to propose that such a thing possibly be added, with the longterm goal of deprecating and removing `ArrayArray#`. The interface for it would look like this:\r\n\r\n{{{#!hs\r\ndata UnliftedArray# (a :: TYPE 'UnliftedRep)\r\ndata MutableUnliftedArray# s (a :: TYPE 'UnliftedRep)\r\n\r\nindexUnliftedArray# :: forall (a :: TYPE 'UnliftedRep). UnliftedArray# a > Int# > a\r\nwriteUnliftedArray# :: forall (a :: TYPE 'UnliftedRep). MutableUnliftedArray# s a > Int# > a > State# s > State# s\r\nreadUnliftedArray# :: forall (a :: TYPE 'UnliftedRep). MutableUnliftedArray# s a > Int# > State# s > (# State# s, a #)\r\nunsafeFreezeUnliftedArray# :: forall (a :: TYPE 'UnliftedRep). MutableUnliftedArray# s a > State# s > (#State# s, UnliftedArray# a#)\r\nnewUnliftedArray# :: forall (a :: TYPE 'UnliftedRep). Int# > a > State# s > (# State# s, MutableUnliftedArray# s a #)\r\n}}}\r\n\r\nYou would also have a few other things like `sameMutableUnliftedArray#`, `sizeofMutableArray#`, `unsafeThawUnliftedArray#`, `copyUnliftedArray#`, etc. The main difficulty that I see in doing this is that I'm not sure if you can tell a primop that it takes a polymorphic argument whose kind is something other than `TYPE LiftedRep`. The bodies of all of the functions I listed above could simply be copied from the `ArrayArray#` functions.\r\n\r\nThere are a few alternatives I've heard discussed. One is to make `Array#` accepted both boxed or unboxed types. There is a brief discussion of this in the UnliftedDataTypes proposal [#point0 (0)]. Indeed, it appears that some have managed to smuggle unlifted data into `Array#` already, with the caveats one would expect [#point1 (1)]. This interface would look like:\r\n\r\n{{{#!hs\r\ndata Array# (a :: TYPE k)\r\ndata MutableArray# s (a :: TYPE k)\r\nindexArray# :: Array# a > Int > a  same as before\r\nindexUnliftedArray# :: forall (a :: TYPE UnliftedRep). Array# a > Int > a\r\n}}}\r\n\r\nSo instead of having `Array#` and `UnliftedArray#` as separate data types, we could have `Array#` handle both cases, but we would need to make a duplicate of every function that operates on `Array#`. This follows all of the appropriate rules for when levity polymorphism is allowed, and it should be backwardscompatible with the previous nonlevitypolymorphic definition of `Array#`. I'm not sure how many things in the GHC runtime assume that the values inside an array are lifted, so this might cause a bunch of problems. If it is possible, this approach would be kind of neat because then `SmallArray#` could be similarly adapted.\r\n\r\nAnyway, I just wanted to get this out there. I would be happy to try implementing the first proposal (involving `UnliftedArray#`) at some point in the next six months. Any feedback on the idea would be appreciated. Also, any comments on how appropriate this is for someone new to contributing to GHC would be appreciated as well. Thanks.\r\n\r\n* [=#point0 (0)] https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes#Parametricity\r\n* [=#point0 (1)] https://www.reddit.com/r/haskell/comments/6v9rmg/an_unified_array_interface/dlyph4i/","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/16468Disabling fprintexplicitruntimereps defaults too much20190321T08:14:29ZKrzysztof GogolewskiDisabling fprintexplicitruntimereps defaults too muchWhen `fprintexplicitruntimereps` is disabled, we instantiate all `RuntimeRep` variables to `LiftedRep` in the entire type. Instead, I think we should do this only for the toplevel foralls  not for the foralls in the contravariant position. Example:
```
λ> foo :: (forall (r :: RuntimeRep). p r) > Int; foo _ = 0
λ> :t foo
foo :: p 'LiftedRep > Int
```
This is not a correct type for `foo`. My expectation is that disabling `fprintexplicitruntimereps` can give a less specific type for an expression, but not an incorrect one.
Related: #16320.When `fprintexplicitruntimereps` is disabled, we instantiate all `RuntimeRep` variables to `LiftedRep` in the entire type. Instead, I think we should do this only for the toplevel foralls  not for the foralls in the contravariant position. Example:
```
λ> foo :: (forall (r :: RuntimeRep). p r) > Int; foo _ = 0
λ> :t foo
foo :: p 'LiftedRep > Int
```
This is not a correct type for `foo`. My expectation is that disabling `fprintexplicitruntimereps` can give a less specific type for an expression, but not an incorrect one.
Related: #16320.