Incorrect missing equation warning (TypeNats)
Summary
GHC does some basic arithmetic reasoning on Wanted constraints via interactTopAdd
. One example is that a Wanted constraint of the form s + t ~ 0
is split into two Wanteds: s ~ 0
and t ~ 0
. This is desirable.
GHC does not do this for Given constraints. If we have [G] s + t ~ 0
, then GHC does not split that into two Givens s ~ 0
and t ~ 0
. This is annoying; see the reproducer below.
After talking with @simonpj, we concluded that probably, tcCheckGivens
should be returning Nothing
more often. To do this properly, a new kind of UnivCoProvenance
probably needs to be defined.
Steps to reproduce
When compiling this program, GHC complains that foo
's matches are not exhaustive, but they actually are because 0
can never match n + 1
. If only GHC could derive that. :)
{-# LANGUAGE DataKinds, GADTs #-}
{-# OPTIONS -Wall #-}
module M where
import Data.Proxy
import GHC.TypeLits
data T n where
Z :: T 0
S :: Proxy n -> T (n + 1)
foo :: T 0 -> Bool
foo Z = True
Playground link: https://play.haskell.org/saved/T78x86vb
Expected behavior
GHC would ideally accept foo
as exhaustive.
Motivation
This is quite important when using GHC TypeLits TypeNats to express the type-level rank of an array in an array library. For example, one might have the following data type for a multidimensional array index:
data Idx n where
ZI :: Idx 0
(::@) :: Int -> Idx n -> Idx (n + 1)
infixr ::@
With GHC's current behaviour, the following function is considered to have non-exhaustive matches:
barIdx :: Idx 2 -> Int
barIdx (i ::@ j ::@ ZI) = i + j
but that means that any user of my array library will get this warning basically everywhere in their code, and there is nothing I can do to fix that. (Except for reporting this issue.)
This code is at https://play.haskell.org/saved/p3JazBQN for playing around.
Environment
- GHC version used: 8.4.4 through 9.10.1