Pattern-match coverage checker mishandles dictionary arguments
It seems that the pattern match coverage checker does not correctly handle dictionary arguments, as evidenced by the following:
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}
import GHC.TypeNats (Nat, KnownNat)
pred1 :: forall (n :: Nat). Int -> Bool
pred1 i = i > 0
pred2 :: forall (n :: Nat). KnownNat n => Int -> Bool
pred2 i = i > 0
foo1 :: Int -> Int
foo1 (pred1 @12 -> True) = 0
foo1 (pred1 @12 -> False) = 0
foo2 :: Int -> Int
foo2 (pred2 @12 -> True) = 0
foo2 (pred2 @12 -> False) = 0
foo1
correctly does not report any pattern match warnings, however foo2
does, because of the dictionary argument:
Pattern match(es) are non-exhaustive
In an equation for ‘foo2’: Patterns not matched: _ :: Int