#15787 closed bug (fixed)

GHC panic using kind application

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.6.2
Component: Compiler Version: 8.6.1
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: polykinds/T15787
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D5275
Wiki Page:

Description

Using GHC head at diff Visible kind application D5229 (#12045),

bug goes away if you remove @ob.

{-# Language RankNTypes #-}
{-# Language TypeApplications #-}
{-# Language DataKinds        #-}
{-# Language PolyKinds        #-}
{-# Language GADTs            #-}
{-# Language TypeFamilies     #-}

import Data.Kind

class Ríki (ob :: Type) where
 type Hom :: ob -> ob -> Type

data
  Kl_kind :: forall ob . (ob -> ob) -> ob -> Type where
  Kl      :: k -> Kl_kind @ob (m) k

type family
  UnKl (kl :: Kl_kind m k) = (res :: k) where
  UnKl (Kl a) = a
$ ghci -ignore-dot-ghci 543_bug.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( 543_bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.7.20181017 for x86_64-unknown-linux):
        ASSERT failed!
  Type-correct unfilled coercion hole {co_a1yH}
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
        pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable
        assertPprPanic, called at compiler/typecheck/TcHsSyn.hs:1805:99 in ghc:TcHsSyn

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

>

Change History (7)

comment:1 Changed 11 months ago by goldfire

Cc: mnguyen added

comment:2 Changed 11 months ago by goldfire

Cc: mnguyen removed
Keywords: TypeInType added; TypeApplications removed

Also not My's fault. The following code panics similarly in HEAD:

{-# Language RankNTypes #-}
{-# Language TypeApplications #-}
{-# Language DataKinds        #-}
{-# Language PolyKinds        #-}
{-# Language GADTs            #-}
{-# Language TypeFamilies     #-}

import Data.Kind

class Ríki (ob :: Type) where
 type Hom :: ob -> ob -> Type

data
  Kl_kind :: forall ob . (ob -> ob) -> ob -> Type where
  Kl      :: k -> Kl_kind (m :: ob -> ob) k

type family
  UnKl (kl :: Kl_kind m k) = (res :: k) where
  UnKl (Kl a) = a

comment:3 Changed 11 months ago by goldfire

Differential Rev(s): Phab:D5275

Patch posted.

comment:4 Changed 11 months ago by Richard Eisenberg <rae@…>

In 4427315/ghc:

Fix #15787 by squashing a coercion hole.

In type-incorrect code, we can sometimes let a coercion
hole make it through the zonker. If this coercion hole then
ends up in the environment (e.g., in the type of a data
constructor), then it causes trouble later.

This patch avoids trouble by substituting the coercion hole
for its representative CoVar. Really, any coercion would do,
but the CoVar was very handy.

test case: polykinds/T15787

comment:5 Changed 11 months ago by goldfire

Status: newmerge
Test Case: polykinds/T15787

Should be easy to merge this one. If it isn't, no worries, as I think it's only an assertion failure.

comment:6 Changed 11 months ago by RyanGlScott

Milestone: 8.6.2

comment:7 Changed 10 months ago by bgamari

Resolution: fixed
Status: mergeclosed

This was merged for 8.6.2 in 7a439e7b13f350e1ac6163f1bfa60e30924dbeea.

Note: See TracTickets for help on using tickets.