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