Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,265
    • Issues 4,265
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 419
    • Merge Requests 419
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Security & Compliance
    • Security & Compliance
    • Dependency List
    • License Compliance
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #18855

Closed
Open
Opened Oct 16, 2020 by Ryan Scott@RyanGlScottMaintainer

GHC 9.0+ regression in checking program with higher-rank kinds

GHC 8.10.2 typechecks the following program:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

import Data.Kind

type TyFun :: Type -> Type -> Type
data TyFun a b

type (~>) :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>

type Apply :: (a ~> b) -> a -> b
type family Apply f x

type Nat :: Type
data Nat = Z | S Nat

type Vec :: Type -> Nat -> Type
data Vec :: Type -> Nat -> Type where
  VNil  :: Vec a Z
  VCons :: a -> Vec a n -> Vec a (S n)

type ElimVec :: forall a.
                forall (p :: forall (k :: Nat). Vec a k ~> Type)
             -> forall (n :: Nat).
                forall (v :: Vec a n)
             -> Apply p VNil
             -> (forall (m :: Nat).
                 forall (x :: a) (xs :: Vec a m) ->
                 Apply p xs ~> Apply p (VCons x xs))
             -> Apply p v
type family ElimVec p v pVNil pVCons where
  forall a (p :: forall (k :: Nat). Vec a k ~> Type)
         (pVNil :: Apply p VNil)
         (pVCons :: forall (m :: Nat).
                    forall (x :: a) (xs :: Vec a m) ->
                    Apply p xs ~> Apply p (VCons x xs)).
    ElimVec p VNil pVNil pVCons = pVNil
  forall a (p :: forall (k :: Nat). Vec a k ~> Type)
         (pVNil :: Apply p VNil)
         (pVCons :: forall (m :: Nat).
                    forall (x :: a) (xs :: Vec a m) ->
                    Apply p xs ~> Apply p (VCons x xs)) l x xs.
    ElimVec p (VCons x (xs :: Vec a l)) pVNil pVCons =
      Apply (pVCons x xs) (ElimVec @a p @l xs pVNil pVCons)

However, GHC 9.0.1-alpha1 and HEAD reject it:

$ ~/Software/ghc-9.0.1-alpha1/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:40:26: error:
    • Couldn't match kind ‘k1’ with ‘m’
      Expected kind ‘Vec a k1’, but ‘xs’ has kind ‘Vec a m’
        because kind variable ‘m’ would escape its scope
      This (rigid, skolem) kind variable is bound by
        ‘forall (m :: Nat).
         forall (x :: a) (xs :: Vec a m) ->
         Apply p xs ~> Apply p (VCons x xs)’
        at Bug.hs:(38,18)-(40,51)
    • In the second argument of ‘Apply’, namely ‘xs’
      In the first argument of ‘(~>)’, namely ‘Apply p xs’
      In a standalone kind signature for ‘ElimVec’:
        forall a.
        forall (p :: forall (k :: Nat). Vec a k ~> Type) ->
        forall (n :: Nat).
        forall (v :: Vec a n) ->
        Apply p VNil
        -> (forall (m :: Nat).
            forall (x :: a) (xs :: Vec a m) ->
            Apply p xs ~> Apply p (VCons x xs))
           -> Apply p v
   |
40 |                  Apply p xs ~> Apply p (VCons x xs))
   |                          ^^

Bug.hs:41:25: error:
    • Couldn't match kind ‘k0’ with ‘n’
      Expected kind ‘Vec a k0’, but ‘v’ has kind ‘Vec a n’
        because kind variable ‘n’ would escape its scope
      This (rigid, skolem) kind variable is bound by
        ‘forall (n :: Nat).
         forall (v :: Vec a n) ->
         Apply p VNil
         -> (forall (m :: Nat).
             forall (x :: a) (xs :: Vec a m) ->
             Apply p xs ~> Apply p (VCons x xs))
            -> Apply p v’
        at Bug.hs:(35,17)-(41,25)
    • In the second argument of ‘Apply’, namely ‘v’
      In a standalone kind signature for ‘ElimVec’:
        forall a.
        forall (p :: forall (k :: Nat). Vec a k ~> Type) ->
        forall (n :: Nat).
        forall (v :: Vec a n) ->
        Apply p VNil
        -> (forall (m :: Nat).
            forall (x :: a) (xs :: Vec a m) ->
            Apply p xs ~> Apply p (VCons x xs))
           -> Apply p v
   |
41 |              -> Apply p v
   |                         ^
Assignee
Assign to
9.0.1
Milestone
9.0.1 (Past due)
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#18855