LiberalTypeSynonyms unsaturation check doesn't kick in
GHC accepts this program:
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
module Bug where
import GHC.Exts (Any)
type KindOf (a :: k) = k
type A a = (Any :: a)
type KA = KindOf A
But it really oughtn't to. After all, we have an unsaturated use of A
in KindOf A
, and we don't have LiberalTypeSynonyms
enabled!
What's even stranger is that there seems to be something about this exact setup that sneaks by LiberalTypeSynonyms
' validity checks. If I add another argument to A
:
type A x a = (Any :: a)
Then it //does// error:
$ /opt/ghc/8.6.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:10:1: error:
• Illegal polymorphic type: forall a -> a
Perhaps you intended to use LiberalTypeSynonyms
• In the type synonym declaration for ‘KA’
|
10 | type KA = KindOf A
| ^^^^^^^^^^^^^^^^^^
Similarly, if I use something besides KindOf
:
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
module Bug where
import GHC.Exts (Any)
type A a = (Any :: a)
type B a = Int
type C = B A
Then I also get the same Illegal polymorphic type: forall a -> a
error.
Trac metadata
Trac field | Value |
---|---|
Version | 8.6.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |