GHC issueshttps://gitlab.haskell.org/ghc/ghc/issues20200125T02:52:26Zhttps://gitlab.haskell.org/ghc/ghc/issues/17670Levitypolymorphism checker is too aggressive for uses of `coerce` on levity...20200125T02:52:26Zlexi.lambdaLevitypolymorphism 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/17723Using default methods with (r ~ LiftedRep) leads to Iface Lint failure20200122T15:06:56ZRyan 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/17675eqType fails on comparing FunTys20200122T09:00:19ZRichard 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/17201Levity polymorphism and defaulting20200106T23:29:28ZKrzysztof GogolewskiLevity polymorphism and defaultingThis ticket concerns two closely related items regarding levity polymorphism.
1. Consider
```
f :: forall p (r :: RuntimeRep). p r > p r
f x = x
g = f
```
Currently, `g` is inferred to be `p 'LiftedRep > p 'LiftedRep`. However, there is no good reason to restrict `r` to `LiftedRep`.
The current strategy is to default all variables of kind `RuntimeRep`. If I define a type family `T` such that `type instance T = RuntimeRep` and change `f` to use `T` instead of `RuntimeRep`, then `g` becomes polymorphic in `r`.
Proposed alternative: when we typecheck a binder, we unify the kind of its type with `TYPE q`. Mark all such variables `q`, and only such variables, for defaulting.
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. The type of `f` would be `forall (a :: TYPE q). a > a`, where `q` is a weakly polymorphic variable, that must be instantiated.
This could be implemented with a special constraint, say `KnownRuntimeRep` that would have to be instantiated (could not be quantified over). That would make the levity restriction in line with the French approach of generating and solving constraints, rather than being an ad hoc defaulting step.
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.This ticket concerns two closely related items regarding levity polymorphism.
1. Consider
```
f :: forall p (r :: RuntimeRep). p r > p r
f x = x
g = f
```
Currently, `g` is inferred to be `p 'LiftedRep > p 'LiftedRep`. However, there is no good reason to restrict `r` to `LiftedRep`.
The current strategy is to default all variables of kind `RuntimeRep`. If I define a type family `T` such that `type instance T = RuntimeRep` and change `f` to use `T` instead of `RuntimeRep`, then `g` becomes polymorphic in `r`.
Proposed alternative: when we typecheck a binder, we unify the kind of its type with `TYPE q`. Mark all such variables `q`, and only such variables, for defaulting.
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. The type of `f` would be `forall (a :: TYPE q). a > a`, where `q` is a weakly polymorphic variable, that must be instantiated.
This could be implemented with a special constraint, say `KnownRuntimeRep` that would have to be instantiated (could not be quantified over). That would make the levity restriction in line with the French approach of generating and solving constraints, rather than being an ad hoc defaulting step.
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.https://gitlab.haskell.org/ghc/ghc/issues/15532Relaxing LevityPolymorphic Binder Check for Lifted vs Unlifted pointers20191202T22:47:48ZAndrew 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/17310Make sameNat and sameSymbol proxypolymorphic20191129T22:47:02ZBodigrimMake sameNat and sameSymbol proxypolymorphic## Motivation
Currently `base:GHC.TypeNats.sameNat` is implemented as follows:
```haskell
sameNat :: (KnownNat a, KnownNat b) => Proxy a > Proxy b > Maybe (a :~: b)
sameNat x y
 natVal x == natVal y = Just (unsafeCoerce Refl)
 otherwise = Nothing
```
One cannot directly apply `sameNat` to a value of type `Foo (a :: Nat)`, but has to bind `a` and construct `Proxy :: Proxy a` first. While not terribly inconvenient, it would be so much better to apply `sameNat` to `Foo a` directly.
The same shortcoming cripples `base:GHC.TypeLits.sameSymbol`.
## Proposal
I propose to change types to
```haskell
sameNat :: (KnownNat a, KnownNat b) => proxy1 a > proxy2 b > Maybe (a :~: b)
sameSymbol :: (KnownSymbol a, KnownSymbol b) => proxy1 a > proxy2 b > Maybe (a :~: b)
```
It does not require any changes in the implementation, because `natVal` and `symbolVal` are already "proxypolymorphic":
```haskell
natVal :: forall n proxy. KnownNat n => proxy n > Natural
symbolVal :: forall n proxy. KnownSymbol n => proxy n > String
```

Discussion in the mail list: https://mail.haskell.org/pipermail/libraries/2019August/029847.html## Motivation
Currently `base:GHC.TypeNats.sameNat` is implemented as follows:
```haskell
sameNat :: (KnownNat a, KnownNat b) => Proxy a > Proxy b > Maybe (a :~: b)
sameNat x y
 natVal x == natVal y = Just (unsafeCoerce Refl)
 otherwise = Nothing
```
One cannot directly apply `sameNat` to a value of type `Foo (a :: Nat)`, but has to bind `a` and construct `Proxy :: Proxy a` first. While not terribly inconvenient, it would be so much better to apply `sameNat` to `Foo a` directly.
The same shortcoming cripples `base:GHC.TypeLits.sameSymbol`.
## Proposal
I propose to change types to
```haskell
sameNat :: (KnownNat a, KnownNat b) => proxy1 a > proxy2 b > Maybe (a :~: b)
sameSymbol :: (KnownSymbol a, KnownSymbol b) => proxy1 a > proxy2 b > Maybe (a :~: b)
```
It does not require any changes in the implementation, because `natVal` and `symbolVal` are already "proxypolymorphic":
```haskell
natVal :: forall n proxy. KnownNat n => proxy n > Natural
symbolVal :: forall n proxy. KnownSymbol n => proxy n > String
```

Discussion in the mail list: https://mail.haskell.org/pipermail/libraries/2019August/029847.htmlhttps://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/13105Allow type families in RuntimeReps20191105T12:18:00ZRichard 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/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/17178Levity Polymorphic Pattern Synonyms20190912T22:38:32ZAndrew 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/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.