"No skolem info" panic when matching on too few fields of a GADT constructor
Summary
When matching on too few fields of a constructor, instead of "Constructor Foo should have 2 arguments, but has been given 1" I get a compiler panic.
Steps to reproduce
This program typechecks just fine:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Bug where
data Foo a b where
Foo :: Bar a b c -> Foo as c -> Foo (a,as) b
data Bar a b c where
data HList xs where
Nil :: HList ()
Cons :: x -> HList xs -> HList (x,xs)
data EqualLists xs ys where
Refl :: EqualLists () ()
ConsRefl :: EqualLists xs ys -> EqualLists (x,xs) (x,ys)
-- matching on ConsRefl provides the proof that the head of the two lists are the same type
-- we bring the types of the tails in scope in the pattern matches and use those in the type of k
foo :: EqualLists xs ys -> HList xs -> HList ys -> Foo xs b -> Foo ys b
foo (ConsRefl equal) (Cons _ (xs :: HList xs)) (Cons _ (ys :: HList ys)) f =
let k :: forall d. Foo xs d -> Foo ys d
k = foo equal xs ys
in case f of
Foo bar foo -> Foo bar $ k foo
But, if we forget to match on bar
in the final line:
Foo foo -> Foo bar $ k foo
We instead get a panic:
ghc: panic! (the 'impossible' happened)
(GHC version 9.0.1:
No skolem info:
[xs_acMw[ssk:3]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Outputable.hs:1230:37 in ghc:GHC.Utils.Outputable
pprPanic, called at compiler/GHC/Tc/Errors.hs:2810:17 in ghc:GHC.Tc.Errors
I tried to minimise the example to only require a few extensions and no imports, but it was difficult to simplify further without knowing what goes wrong.
Expected behavior
"Constructor Foo should have 2 arguments, but has been given 1"
Environment
- GHC version used: 9.0.1