Opened 8 months ago

Last modified 2 months ago

#16247 new bug

GHC 8.6 Core Lint regression (Kind application error)

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.10.1
Component: Compiler (Type checker) Version: 8.6.3
Keywords: TypeInType Cc: simonpj
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash or panic Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

The following program produces a Core Lint error on GHC 8.6.3 and HEAD:

{-# 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
  |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Change History (3)

comment:1 Changed 8 months ago by RyanGlScott

Cc: simonpj added

This regression was introduced in commit 2bbdd00c6d70bdc31ff78e2a42b26159c8717856 (Orient TyVar/TyVar equalities with deepest on the left).

comment:2 Changed 7 months ago by RyanGlScott

A more complicated example that singletons spat out:

{-# 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] <k_a2U7>_N) <p_a2U6>_N’
      Function kind = k_a2U7 -> *
      Arg kinds = [(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] <k_a2U7>_N) <p_a2U6>_N’
      Function kind = k_a2U7 -> *
      Arg kinds = [(p_a2U6, k_a2U5)]
    Fun: k_a2U7
         (p_a2U6, k_a2U5)
Bug.hs:22:36: warning:
    [in body of lambda with binder z_X1QM :: TyFun
                                               (U1 p_a2U6)
                                               (M1
                                                  D
                                                  ('MetaData "U1" "GHC.Generics" "base" 'False)
                                                  (C1 ('MetaCons "U1" 'PrefixI 'False) U1)
                                                  p_a2U6)]
    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)
Bug.hs:22:36: warning:
    [in body of lambda with binder z_X1QM :: TyFun
                                               (U1 p_a2U6)
                                               (M1
                                                  D
                                                  ('MetaData "U1" "GHC.Generics" "base" 'False)
                                                  (C1 ('MetaCons "U1" 'PrefixI 'False) U1)
                                                  p_a2U6)]
    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 expression: From1Sym0KindInference
                         @ k_a2U5
                         @ p_a2U6
                         @ k_a2U7
                         @ (z_X1QM |> (TyFun
                                         <U1 p_a2U6>_N (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)
                         @ k_X2TZ
                         @ p_X2U5
                         @ z_X1QM
                         @ arg_X1QO
                         @~ (<(z_X1QM |> (TyFun
                                            <U1 p_a2U6>_N
                                            (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)>_N
                             :: (z_X1QM |> (TyFun
                                              <U1 p_a2U6>_N
                                              (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)
                                ~# (z_X1QM |> (TyFun
                                                 <U1 p_a2U6>_N
                                                 (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N))
                         dt_a35M
    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 expression: From1Sym0KindInference
                         @ k_a2U5
                         @ p_a2U6
                         @ k_a2U7
                         @ (z_X1QM |> (TyFun
                                         <U1 p_a2U6>_N (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)
                         @ k_X2TZ
                         @ p_X2U5
                         @ z_X1QM
                         @ arg_X1QO
                         @~ (<(z_X1QM |> (TyFun
                                            <U1 p_a2U6>_N
                                            (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)>_N
                             :: (z_X1QM |> (TyFun
                                              <U1 p_a2U6>_N
                                              (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)
                                ~# (z_X1QM |> (TyFun
                                                 <U1 p_a2U6>_N
                                                 (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N))
                         dt_a35M
    Kind application error in
      coercion ‘Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N’
      Function kind = k_a2U7 -> *
      Arg kinds = [(p_a2U6, k_a2U5)]
    Fun: k_a2U7
         (p_a2U6, k_a2U5)
<no location info>: warning:
    In the expression: From1Sym0KindInference
                         @ k_a2U5
                         @ p_a2U6
                         @ k_a2U7
                         @ (z_X1QM |> (TyFun
                                         <U1 p_a2U6>_N (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)
                         @ k_X2TZ
                         @ p_X2U5
                         @ z_X1QM
                         @ arg_X1QO
                         @~ (<(z_X1QM |> (TyFun
                                            <U1 p_a2U6>_N
                                            (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)>_N
                             :: (z_X1QM |> (TyFun
                                              <U1 p_a2U6>_N
                                              (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)
                                ~# (z_X1QM |> (TyFun
                                                 <U1 p_a2U6>_N
                                                 (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N))
                         dt_a35M
    Kind application error in
      coercion ‘Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N’
      Function kind = k_a2U7 -> *
      Arg kinds = [(p_a2U6, k_a2U5)]
    Fun: k_a2U7
         (p_a2U6, k_a2U5)
<no location info>: warning:
    In the coercion ‘<(z_X1QM |> (TyFun
                                    <U1 p_a2U6>_N (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_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 coercion ‘<(z_X1QM |> (TyFun
                                    <U1 p_a2U6>_N (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)>_N’
    Kind application error in
      coercion ‘Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N’
      Function kind = k_a2U7 -> *
      Arg kinds = [(p_a2U6, k_a2U5)]
    Fun: k_a2U7
         (p_a2U6, k_a2U5)
<no location info>: warning:
    In the coercion ‘<(z_X1QM |> (TyFun
                                    <U1 p_a2U6>_N (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)>_N’
    Kind application error in
      coercion ‘Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N’
      Function kind = k_a2U7 -> *
      Arg kinds = [(p_a2U6, k_a2U5)]
    Fun: k_a2U7
         (p_a2U6, k_a2U5)
Bug.hs:22:36: warning:
    [in body of lambda with binder z_X1QM :: TyFun
                                               (U1 p_a2U6)
                                               (M1
                                                  D
                                                  ('MetaData "U1" "GHC.Generics" "base" 'False)
                                                  (C1 ('MetaCons "U1" 'PrefixI 'False) U1)
                                                  p_a2U6)]
    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)
Bug.hs:22:36: warning:
    [in body of lambda with binder z_X1QM :: TyFun
                                               (U1 p_a2U6)
                                               (M1
                                                  D
                                                  ('MetaData "U1" "GHC.Generics" "base" 'False)
                                                  (C1 ('MetaCons "U1" 'PrefixI 'False) U1)
                                                  p_a2U6)]
    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 expression: From1Sym0KindInference
                         @ k_a2U5
                         @ p_a2U6
                         @ k_a2U7
                         @ (z_X1QM |> (TyFun
                                         <U1 p_a2U6>_N (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)
                         @ k_X2TZ
                         @ p_X2U5
                         @ z_X1QM
                         @ arg_X1QO
                         @~ (<(z_X1QM |> (TyFun
                                            <U1 p_a2U6>_N
                                            (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)>_N
                             :: (z_X1QM |> (TyFun
                                              <U1 p_a2U6>_N
                                              (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)
                                ~# (z_X1QM |> (TyFun
                                                 <U1 p_a2U6>_N
                                                 (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N))
                         dt_a35M
    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 expression: From1Sym0KindInference
                         @ k_a2U5
                         @ p_a2U6
                         @ k_a2U7
                         @ (z_X1QM |> (TyFun
                                         <U1 p_a2U6>_N (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)
                         @ k_X2TZ
                         @ p_X2U5
                         @ z_X1QM
                         @ arg_X1QO
                         @~ (<(z_X1QM |> (TyFun
                                            <U1 p_a2U6>_N
                                            (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)>_N
                             :: (z_X1QM |> (TyFun
                                              <U1 p_a2U6>_N
                                              (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)
                                ~# (z_X1QM |> (TyFun
                                                 <U1 p_a2U6>_N
                                                 (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N))
                         dt_a35M
    Kind application error in
      coercion ‘Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N’
      Function kind = k_a2U7 -> *
      Arg kinds = [(p_a2U6, k_a2U5)]
    Fun: k_a2U7
         (p_a2U6, k_a2U5)
<no location info>: warning:
    In the expression: From1Sym0KindInference
                         @ k_a2U5
                         @ p_a2U6
                         @ k_a2U7
                         @ (z_X1QM |> (TyFun
                                         <U1 p_a2U6>_N (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)
                         @ k_X2TZ
                         @ p_X2U5
                         @ z_X1QM
                         @ arg_X1QO
                         @~ (<(z_X1QM |> (TyFun
                                            <U1 p_a2U6>_N
                                            (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)>_N
                             :: (z_X1QM |> (TyFun
                                              <U1 p_a2U6>_N
                                              (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)
                                ~# (z_X1QM |> (TyFun
                                                 <U1 p_a2U6>_N
                                                 (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N))
                         dt_a35M
    Kind application error in
      coercion ‘Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N’
      Function kind = k_a2U7 -> *
      Arg kinds = [(p_a2U6, k_a2U5)]
    Fun: k_a2U7
         (p_a2U6, k_a2U5)
<no location info>: warning:
    In the coercion ‘<(z_X1QM |> (TyFun
                                    <U1 p_a2U6>_N (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_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 coercion ‘<(z_X1QM |> (TyFun
                                    <U1 p_a2U6>_N (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)>_N’
    Kind application error in
      coercion ‘Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N’
      Function kind = k_a2U7 -> *
      Arg kinds = [(p_a2U6, k_a2U5)]
    Fun: k_a2U7
         (p_a2U6, k_a2U5)
<no location info>: warning:
    In the coercion ‘<(z_X1QM |> (TyFun
                                    <U1 p_a2U6>_N (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)>_N’
    Kind application error in
      coercion ‘Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N’
      Function kind = k_a2U7 -> *
      Arg kinds = [(p_a2U6, k_a2U5)]
    Fun: k_a2U7
         (p_a2U6, k_a2U5)
*** Offending Program ***
$WFrom1Sym0KindInference [InlPrag=INLINE[2]]
  :: 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)
[GblId[DataConWrapper],
 Arity=1,
 Caf=NoCafRefs,
 Str=<L,U>,
 Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True,
         Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=False)
         Tmpl= \ (@ k_X2TZ)
                 (@ (p_X2U5 :: k_X2TZ))
                 (@ k_a2U5)
                 (@ k_a2U7)
                 (@ (p_a2U6 :: k_a2U5))
                 (@ (z_X1QM :: TyFun
                                 (U1 p_a2U6)
                                 (M1
                                    D
                                    ('MetaData "U1" "GHC.Generics" "base" 'False)
                                    (C1 ('MetaCons "U1" 'PrefixI 'False) U1)
                                    p_a2U6)))
                 (@ (arg_X1QO :: U1 p_X2U5))
                 (dt_a35M [Occ=Once]
                    :: SameKind
                         (Apply
                            (From1U1Sym0 |> (TyFun
                                               <U1 p_X2U5>_N
                                               (Sym (Sym (Rep1_U1[0] <k_X2TZ>_N) <p_X2U5>_N)))_N
                                            ->_N <*>_N)
                            arg_X1QO)
                         (From1U1 arg_X1QO |> Sym (Sym (Rep1_U1[0]
                                                            <k_X2TZ>_N) <p_X2U5>_N))) ->
                 From1Sym0KindInference
                   @ k_a2U5
                   @ p_a2U6
                   @ k_a2U7
                   @ (z_X1QM |> (TyFun
                                   <U1 p_a2U6>_N (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)
                   @ k_X2TZ
                   @ p_X2U5
                   @ z_X1QM
                   @ arg_X1QO
                   @~ (<(z_X1QM |> (TyFun
                                      <U1 p_a2U6>_N (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)>_N
                       :: (z_X1QM |> (TyFun
                                        <U1 p_a2U6>_N (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)
                          ~# (z_X1QM |> (TyFun
                                           <U1 p_a2U6>_N
                                           (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N))
                   dt_a35M}]
$WFrom1Sym0KindInference
  = \ (@ k_X2TZ)
      (@ (p_X2U5 :: k_X2TZ))
      (@ k_a2U5)
      (@ k_a2U7)
      (@ (p_a2U6 :: k_a2U5))
      (@ (z_X1QM :: TyFun
                      (U1 p_a2U6)
                      (M1
                         D
                         ('MetaData "U1" "GHC.Generics" "base" 'False)
                         (C1 ('MetaCons "U1" 'PrefixI 'False) U1)
                         p_a2U6)))
      (@ (arg_X1QO :: U1 p_X2U5))
      (dt_a35M [Occ=Once]
         :: SameKind
              (Apply
                 (From1U1Sym0 |> (TyFun
                                    <U1 p_X2U5>_N (Sym (Sym (Rep1_U1[0] <k_X2TZ>_N) <p_X2U5>_N)))_N
                                 ->_N <*>_N)
                 arg_X1QO)
              (From1U1 arg_X1QO |> Sym (Sym (Rep1_U1[0]
                                                 <k_X2TZ>_N) <p_X2U5>_N))) ->
      From1Sym0KindInference
        @ k_a2U5
        @ p_a2U6
        @ k_a2U7
        @ (z_X1QM |> (TyFun
                        <U1 p_a2U6>_N (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)
        @ k_X2TZ
        @ p_X2U5
        @ z_X1QM
        @ arg_X1QO
        @~ (<(z_X1QM |> (TyFun
                           <U1 p_a2U6>_N (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)>_N
            :: (z_X1QM |> (TyFun
                             <U1 p_a2U6>_N (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N)
               ~# (z_X1QM |> (TyFun
                                <U1 p_a2U6>_N (Sym (Rep1_U1[0] <k_a2U7>_N) <p_a2U6>_N))_N))
        dt_a35M

$trModule1_r36E :: Addr#
[GblId, Caf=NoCafRefs, Unf=OtherCon []]
$trModule1_r36E = "main"#

$trModule2_r36Q :: TrName
[GblId, Caf=NoCafRefs, Unf=OtherCon []]
$trModule2_r36Q = TrNameS $trModule1_r36E

$trModule3_r36R :: Addr#
[GblId, Caf=NoCafRefs, Unf=OtherCon []]
$trModule3_r36R = "Bug"#

$trModule4_r36S :: TrName
[GblId, Caf=NoCafRefs, Unf=OtherCon []]
$trModule4_r36S = TrNameS $trModule3_r36R

$trModule :: Module
[GblId, Caf=NoCafRefs, Unf=OtherCon []]
$trModule = Module $trModule2_r36Q $trModule4_r36S

$tcTyFun1_r36T :: Addr#
[GblId, Caf=NoCafRefs, Unf=OtherCon []]
$tcTyFun1_r36T = "TyFun"#

$tcTyFun2_r36U :: TrName
[GblId, Caf=NoCafRefs, Unf=OtherCon []]
$tcTyFun2_r36U = TrNameS $tcTyFun1_r36T

$tcTyFun :: TyCon
[GblId, Unf=OtherCon []]
$tcTyFun
  = TyCon
      8840097126617362261##
      15320025594455375939##
      $trModule
      $tcTyFun2_r36U
      0#
      krep$*->*->*

*** End of Offense ***


<no location info>: error: 
Compilation had errors

comment:3 Changed 2 months ago by Marge Bot <ben+marge-bot@…>

In 80afdf6/ghc:

Fix over-eager implication constraint discard

Ticket #16247 showed that we were discarding an implication
constraint that had empty ic_wanted, when we still needed to
keep it so we could check whether it had a bad telescope.

Happily it's a one line fix.  All the rest is comments!
Note: See TracTickets for help on using tickets.