GitLab

Compile the following program with GHC HEAD:

{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall #-}
module Bug where

import Data.Type.Equality

f :: a :~: Int -> b :~: Bool -> a :~: b -> void
f Refl Refl x = case x of {}

$([d| g :: a :~: Int -> b :~: Bool -> a :~: b -> void
      g Refl Refl x = case x of {}
    |])

And you'll get a warning, surprisingly enough:

$ ~/Software/ghc5/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o, Bug.dyn_o )

Bug.hs:13:3: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: Refl
   |
13 | $([d| g :: a :~: Int -> b :~: Bool -> a :~: b -> void
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

This is unusual because f and g have the same definition and both should be deemed exhaustive, since nothing inhabits the type Int :~: Bool. The only difference between f and g is that the latter function is defined using Template Haskell quotes.

This is a regression from GHC 8.8.1 and earlier, which do not produce any warnings for either function.

cc @sgraf812