No skolem info panic involving typed hole
The following program causes a No skolem info
panic on GHC 9.0.1, 9.2.1, HEAD, but not on GHC 8.10.5.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
data Context where
Extend :: forall k. Context -> Context
type (:*&) :: Context -> forall k -> Context
type ctx :*& k = Extend @k ctx
data Idx ctx where
T :: Idx ctx -> Idx (ctx :*& l)
data Rn ctx1 ctx2 where
U :: Rn ctx1 ctx2 -> Rn (ctx1 :*& l) (ctx2 :*& l)
rnRename :: Rn ctx1 ctx2 -> Idx ctx3 -> Idx ctx4
rnRename (U _ ) _ = T _
rnRename _ T = undefined
[1 of 1] Compiling Bug ( src\Bug.hs, interpreted )
ghc.exe: panic! (the 'impossible' happened)
(GHC version 9.0.1:
No skolem info:
[ctx4_aBB[sk:1]]
The program should be rejected, and the error given with GHC 8.10.5 seems perfect:
[1 of 1] Compiling Bug ( src\Bug.hs, interpreted )
src\Bug.hs:26:17: error:
• The constructor ‘T’ should have 1 argument, but has been given none
• In the pattern: T
In an equation for ‘rnRename’: rnRename _ T = undefined
|
26 | rnRename _ T = undefined
| ^
The issue seems to be related to the presence of a typed hole on the line prior to the bogus pattern match.