[GHC] #16247: GHC 8.6 Core Lint regression (Kind application error)
#16247: GHC 8.6 Core Lint regression (Kind application error) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.10.1 Component: Compiler | Version: 8.6.3 (Type checker) | Keywords: TypeInType | Operating System: Unknown/Multiple Architecture: | Type of failure: Compile-time Unknown/Multiple | crash or panic Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The following program produces a Core Lint error on GHC 8.6.3 and HEAD: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind data SameKind :: forall k. k -> k -> Type data Foo :: forall a k (b :: k). SameKind a b -> Type where MkFoo :: Foo sameKind }}} {{{ $ /opt/ghc/8.6.3/bin/ghc Bug.hs -dcore-lint [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) *** Core Lint errors : in result of CorePrep *** <no location info>: warning: In the type ‘forall k (a :: k) k (b :: k) (sameKind :: SameKind a b). Foo sameKind’ Kind application error in type ‘SameKind a_aWE b_aWG’ Function kind = forall k. k -> k -> * Arg kinds = [(k_aWF, *), (a_aWE, k_aWD), (b_aWG, k_aWF)] Fun: k_aWF (a_aWE, k_aWD) *** Offending Program *** <elided> MkFoo :: forall k (a :: k) k (b :: k) (sameKind :: SameKind a b). Foo sameKind }}} (Confusingly, the type of `MkFoo` is rendered as `forall k (a :: k) k (b :: k) (sameKind :: SameKind a b). Foo sameKind` in that `-dcore-lint` error, but I think it really should be `forall k1 (a :: k1) k2 (b :: k2) (sameKind :: SameKind a b). Foo sameKind`.) On GHC 8.4.4 and earlier, this simply produces an error message: {{{ $ /opt/ghc/8.4.4/bin/ghc Bug.hs -dcore-lint [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:9:13: error: • These kind and type variables: a k (b :: k) are out of dependency order. Perhaps try this ordering: k (a :: k) (b :: k) • In the kind ‘forall a k (b :: k). SameKind a b -> Type’ | 9 | data Foo :: forall a k (b :: k). SameKind a b -> Type where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16247 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16247: GHC 8.6 Core Lint regression (Kind application error) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.10.1 Component: Compiler (Type | Version: 8.6.3 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: simonpj (added) Comment: This regression was introduced in commit 2bbdd00c6d70bdc31ff78e2a42b26159c8717856 (`Orient TyVar/TyVar equalities with deepest on the left`). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16247#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16247: GHC 8.6 Core Lint regression (Kind application error)
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone: 8.10.1
Component: Compiler (Type | Version: 8.6.3
checker) |
Resolution: | Keywords: TypeInType
Operating System: Unknown/Multiple | Architecture:
Type of failure: Compile-time | Unknown/Multiple
crash or panic | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by RyanGlScott):
A more complicated example that `singletons` spat out:
{{{#!hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind (Constraint, Type)
import GHC.Generics (Rep1, U1(..))
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: a ~> b) (x :: a) :: b
type SameKind (a :: k) (b :: k) = (() :: Constraint)
type family From1 (z :: (f :: Type -> Type) a) :: Rep1 f a
type family From1U1 (x :: U1 (p :: k)) :: Rep1 U1 p where {}
data From1U1Sym0 :: forall p k. (U1 :: k -> Type) p ~> Rep1 (U1 :: k ->
Type) p where
From1Sym0KindInference :: forall z arg. SameKind (Apply From1U1Sym0 arg)
(From1U1 arg)
=> From1U1Sym0 z
}}}
{{{
$ /opt/ghc/8.6.3/bin/ghc Bug.hs -dcore-lint
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Tidy Core ***
<no location info>: warning:
In the type ‘forall k (p :: k) k k (p :: k) (z :: TyFun
(U1 p)
(M1
D
('MetaData
"U1"
"GHC.Generics" "base" 'False)
(C1 ('MetaCons
"U1" 'PrefixI 'False) U1)
p)) (arg :: U1
p).
SameKind
(Apply
(From1U1Sym0 |> (TyFun
<U1 p>_N (Sym (Sym (Rep1_U1[0]
<k>_N) <p>_N)))_N
->_N <*>_N)
arg)
(From1U1 arg |> Sym (Sym (Rep1_U1[0] <k>_N) <p>_N)) =>
From1U1Sym0
(z |> (TyFun <U1 p>_N (Sym (Rep1_U1[0] <k>_N)
<p>_N))_N)’
Kind application error in type ‘U1 p_a2U6’
Function kind = forall k. k -> *
Arg kinds = [(k_a2U7, *), (p_a2U6, k_a2U5)]
Fun: k_a2U7
(p_a2U6, k_a2U5)
<no location info>: warning:
In the type ‘forall k (p :: k) k k (p :: k) (z :: TyFun
(U1 p)
(M1
D
('MetaData
"U1"
"GHC.Generics" "base" 'False)
(C1 ('MetaCons
"U1" 'PrefixI 'False) U1)
p)) (arg :: U1
p).
SameKind
(Apply
(From1U1Sym0 |> (TyFun
<U1 p>_N (Sym (Sym (Rep1_U1[0]
<k>_N) <p>_N)))_N
->_N <*>_N)
arg)
(From1U1 arg |> Sym (Sym (Rep1_U1[0] <k>_N) <p>_N)) =>
From1U1Sym0
(z |> (TyFun <U1 p>_N (Sym (Rep1_U1[0] <k>_N)
<p>_N))_N)’
Kind application error in
type ‘M1
D
('MetaData "U1" "GHC.Generics" "base" 'False)
(C1 ('MetaCons "U1" 'PrefixI 'False) U1)
p_a2U6’
Function kind = forall k. * -> Meta -> (k -> *) -> k -> *
Arg kinds = [(k_a2U7, *), (D, *),
('MetaData "U1" "GHC.Generics" "base" 'False, Meta),
(C1 ('MetaCons "U1" 'PrefixI 'False) U1, k_a2U7 -> *),
(p_a2U6, k_a2U5)]
Fun: k_a2U7
(p_a2U6, k_a2U5)
<no location info>: warning:
In the type ‘forall k (p :: k) k k (p :: k) (z :: TyFun
(U1 p)
(M1
D
('MetaData
"U1"
"GHC.Generics" "base" 'False)
(C1 ('MetaCons
"U1" 'PrefixI 'False) U1)
p)) (arg :: U1
p).
SameKind
(Apply
(From1U1Sym0 |> (TyFun
<U1 p>_N (Sym (Sym (Rep1_U1[0]
<k>_N) <p>_N)))_N
->_N <*>_N)
arg)
(From1U1 arg |> Sym (Sym (Rep1_U1[0] <k>_N) <p>_N)) =>
From1U1Sym0
(z |> (TyFun <U1 p>_N (Sym (Rep1_U1[0] <k>_N)
<p>_N))_N)’
Kind application error in type ‘U1 p_a2U6’
Function kind = forall k. k -> *
Arg kinds = [(k_a2U7, *), (p_a2U6, k_a2U5)]
Fun: k_a2U7
(p_a2U6, k_a2U5)
<no location info>: warning:
In the type ‘forall k (p :: k) k k (p :: k) (z :: TyFun
(U1 p)
(M1
D
('MetaData
"U1"
"GHC.Generics" "base" 'False)
(C1 ('MetaCons
"U1" 'PrefixI 'False) U1)
p)) (arg :: U1
p).
SameKind
(Apply
(From1U1Sym0 |> (TyFun
<U1 p>_N (Sym (Sym (Rep1_U1[0]
<k>_N) <p>_N)))_N
->_N <*>_N)
arg)
(From1U1 arg |> Sym (Sym (Rep1_U1[0] <k>_N) <p>_N)) =>
From1U1Sym0
(z |> (TyFun <U1 p>_N (Sym (Rep1_U1[0] <k>_N)
<p>_N))_N)’
Kind application error in
coercion ‘Sym (Rep1_U1[0]
participants (1)
-
GHC