Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,826
    • Issues 4,826
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 443
    • Merge requests 443
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
    • Value stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #16247

Closed
Open
Created Jan 27, 2019 by Ryan Scott@RyanGlScottMaintainer

GHC 8.6 Core Lint regression (Kind application error)

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
  |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Trac metadata
Trac field Value
Version 8.6.3
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking