Deducing different type class constraints in different cases of pattern match

Question

I am trying to use a type family to generate constraints which depend on some type level natural number. Here is such an function:

type family F (n :: Nat) (m :: Nat) :: Constraint where
  F 0 m = ()
  F n m = (m ~ 0)

Then i have a function which has this constraint.

f :: forall n m. (KnownNat n, KnownNat m, m ~ 0) => ()
f = ()

When I am trying to use this function in a pattern match where my type family should produce this constraint, ghc says that it can't deduce the constraint

Here is an example:

g :: forall n m. (KnownNat n, KnownNat m, F n m) => ()
g =
  case (natVal (Proxy @n)) of
    0 -> ()
    n -> f @n @m

It produces the error

• Could not deduce: m ~ 0 arising from a use of ‘f’
      from the context: (KnownNat n, KnownNat m, F n m)
        bound by the type signature for:
                   g :: forall (n :: Nat) (m :: Nat).
                        (KnownNat n, KnownNat m, F n m) =>
                        ()
    ‘m’ is a rigid type variable bound by
        the type signature for:
          g :: forall (n :: Nat) (m :: Nat).
               (KnownNat n, KnownNat m, F n m) =>
               ()
 • In the expression: f @n @m
      In a case alternative: n -> f @n @m
      In the expression:
        case (natVal (Proxy @n)) of
          0 -> ()
          n -> f @n @m
    |
168 |     n -> f @n @m
    |          ^^^^^^^

Answer 1

The main reason your pattern match doesn't produce any constraint is that you're case matching on natVal (Proxy @n) :: Integer which isn't a GADT. As per @chi's answer, you need to match on a GADT to get type information into scope.

For a slightly modified version of your type family:

type family F (n :: Nat) (m :: Nat) :: Constraint where
  F 0 m = (m ~ 0)
  F n m = ()

the way you'd accomplish this would be:

f :: forall n m. (m ~ 0) => ()
f = ()

g :: forall n m. (KnownNat n, F n m) => ()
g = case sameNat (Proxy @n) (Proxy @0) of
  Just Refl -> f @n @m
  Nothing -> ()

This case-matches on a GADT to introduce a constraint n ~ 0 in the Just Refl branch. This allows the type family F n m to be resolved to m ~ 0. Note that I've removed the extraneous KnownNat constraints; this is somewhat important, since @chi's answer shows that your problem is easily solved if you have a KnownNat m constraint available in g's type signature. After all, if m is known, then you can determine directly if it's 0 or not, and the F m n constraint is redundant, regardless of the values of m and n.

Unfortunately, for your original type family with the condition flipped:

type family F (n :: Nat) (m :: Nat) :: Constraint where
  F 0 m = ()
  F n m = (m ~ 0)

things are more difficult. Type families are resolved using a pretty simple "forward solver", for lack of a better term, so for your version of F, the type expression F n m can only be resolved for a specific n, like 0 or 5. There's no constraint expressing the fact that n is an unspecified type other than 0 that you could somehow use to resolve F n m = (m ~ 0). So, you could write:

g :: forall n m. (KnownNat n, F n m) => ()
g = case sameNat (Proxy @n) (Proxy @1) of
      Just Refl -> f @n @m
      Nothing -> ()

which uses the fact that in the Just Refl -> branch, the constraint n ~ 1 is in scope which allows F n m to be resolved. But there doesn't seem to be a way to get it to work for arbitrary non-zero n.

There are a few approaches that would work. Switching to Peano naturals would solve the problem:

data Nat = Z | S Nat
data SNat n where
  SZ :: SNat Z
  SS :: SNat n -> SNat (S n)
class KnownNat n where
  natSing :: SNat n
instance KnownNat Z where natSing = SZ
instance KnownNat n => KnownNat (S n) where natSing = SS natSing

type family F (n :: Nat) (m :: Nat) :: Constraint where
  F Z m = ()
  F (S n) m = (m ~ Z)

f :: forall n m. (m ~ Z) => ()
f = ()

g :: forall n m. (KnownNat n, F n m) => ()
g = case natSing @n of
  SZ -> ()
  SS n -> f @n @m

Here, the SS n case branch brings into scope the constraint n ~ S n1, which does express the fact that n is an unspecified natural other than Z, allowing us to resolve the type family F n m = (m ~ Z).

You could also represent the F constraint using a type-level conditional:

type F n m = If (1 <=? n) (m ~ 0) (() :: Constraint)

and write:

import Data.Kind
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import GHC.TypeLits
import Unsafe.Coerce

type F n m = If (1 <=? n) (m ~ 0) (() :: Constraint)

f :: forall n m. (m ~ 0) => ()
f = ()

g :: forall n m. (KnownNat n, F n m) => ()
g = case leqNat (Proxy @1) (Proxy @n) of
  Just Refl -> f @n @m
  Nothing -> ()

leqNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe ((a <=? b) :~: True)
leqNat x y | natVal x <= natVal y = Just (unsafeCoerce Refl)
           | otherwise            = Nothing

Here, the function leqNat provides the appropriate type-level evidence that one value is less than or equal to another. It probably looks like cheating, but if you compare it to the definition of sameNat, you'll see it's the usual sort of cheating.