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,829
    • Issues 4,829
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 447
    • Merge requests 447
  • 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
  • #15343

Closed
Open
Created Jul 04, 2018 by Ryan Scott@RyanGlScottMaintainer

Implicitly quantifying a kind variable causes GHC 8.6 to panic (coercionKind)

The following program panics on GHC 8.6 and later:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Kind
import Data.Type.Equality

data family Sing :: forall k. k -> Type
data SomeSing :: Type -> Type where
  SomeSing :: Sing (a :: k) -> SomeSing k

class SingKind k where
  type Demote k :: Type
  fromSing :: Sing (a :: k) -> Demote k
  toSing   :: Demote k -> SomeSing k

data instance Sing (z :: a :~~: b) where
  SHRefl :: Sing HRefl

instance SingKind (a :~~: b) where
  type Demote (a :~~: b) = a :~~: b
  fromSing SHRefl = HRefl
  toSing HRefl    = SomeSing SHRefl

data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2

(~>:~~:) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)
                   (p :: forall (z :: Type) (y :: z). (a :~~: y) ~> Type)
                   (r :: a :~~: b).
            Sing r
         -> Apply p HRefl
         -> Apply p r
(~>:~~:) SHRefl pHRefl = pHRefl

type family Why (a :: j) (e :: a :~~: (y :: z)) :: Type where
  Why a (_ :: a :~~: y)  = y :~~: a

data    WhySym (a :: j) :: forall   (y :: z). (a :~~: y) ~> Type
-- data WhySym (a :: j) :: forall z (y :: z). (a :~~: y) ~> Type
-- The version above does NOT panic
type instance Apply (WhySym a) e = Why a e

hsym :: forall (j :: Type) (k :: Type) (a :: j) (b :: k).
        a :~~: b -> b :~~: a
hsym eq = case toSing eq of
            SomeSing (singEq :: Sing r) ->
              (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
  (GHC version 8.6.0.20180627 for x86_64-unknown-linux):
        coercionKind
  Nth:3
      (Inst {co_a1jI} (Coh <k_a1js[sk:1]>_N (Nth:0 (Sym {co_a1jI}))))
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
        pprPanic, called at compiler/types/Coercion.hs:1887:9 in ghc:Coercion

As noted in the comments, replacing WhySym with a version that explicitly quantifies z avoids the panic.

This is a regression from GHC 8.4.3, in which the program simply errored:

$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:56:38: error:
    • Expected kind ‘forall z (y :: z). (a1 :~~: y) ~> *’,
        but ‘WhySym a’ has kind ‘forall (y :: z0).
                                 TyFun (a1 :~~: y) * -> *’
    • In the type ‘(WhySym a)’
      In the expression: (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
      In a case alternative:
          SomeSing (singEq :: Sing r)
            -> (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
    • Relevant bindings include
        singEq :: Sing a2 (bound at Bug.hs:55:23)
        eq :: a1 :~~: b (bound at Bug.hs:54:6)
        hsym :: (a1 :~~: b) -> b :~~: a1 (bound at Bug.hs:54:1)
   |
56 |               (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
   |                                      ^^^^^^^^
Trac metadata
Trac field Value
Version 8.5
Type Bug
TypeOfFailure OtherFailure
Priority high
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