Proof a constraint when using a type family

Question

I have a closed type family that I use to calculate something at the type level. The result of that calculation is only valid if some input passes some constraints and I use a custom TypeError to give a type error if the input is wrong. Here is a simple example:

import Data.Proxy
import GHC.TypeLits
import Data.Bool
import Data.Function

type Foo (a :: Nat) (b :: Nat) = Foo1 (Div a b) (1 <=? b)

type family Foo1 (result :: Nat) (valid :: Bool) :: Nat where
  Foo1 c 'True = c
  Foo1 _ 'False = TypeError ('Text "Oops, divide by zero")


f :: (KnownNat a, KnownNat b, r ~ (Foo a b)) => Proxy a -> Proxy b -> Proxy b
f _ x = g x

g :: (KnownNat a, 1 <= a) => Proxy a -> Proxy a
g = id

Where an explicit check for division by zero is done. Obviously in this case 1 <= b trivially holds since I check for this exact case in my Foo type. This however doesn't compile since GHC doesn't understand this and it can't deduce the 1 <= b constraint:

• Could not deduce: (1 <=? b) ~ 'True arising from a use of ‘g’
      from the context: (KnownNat a, KnownNat b, r ~ Foo a b)
        bound by the type signature for:
                   f :: forall (a :: Nat) (b :: Nat) (r :: Nat).
                        (KnownNat a, KnownNat b, r ~ Foo a b) =>
                        Proxy a -> Proxy b -> Proxy b
        at Test.hs:57:1-77
    • In the expression: g x
      In an equation for ‘f’: f _ x = g x
    • Relevant bindings include
        f :: Proxy a -> Proxy b -> Proxy b (bound at Test.hs:58:1)
   |
58 | f _ x = g x

Is there a way for me to say to GHC "introduce" this constraint since I know for sure it holds? I don't want to write the "1 <= b" in my original type signature because it's essentially duplicate and will also pollute a lot of code that depends on my function with that constraint.

Edit:

I think the Singletons package can do what I want but I just don't know how to express it correctly...

import Data.Proxy
import GHC.TypeLits
import Data.Bool
import GHC.Err

import Data.Singletons.TypeLits ( Sing (SNat), SNat )
import Data.Singletons.Decide
import Data.Singletons.Prelude.Bool
import Data.Kind (Type)

import Data.Singletons.Prelude.Ord ((%<=))

type Foo (a :: Nat) (b :: Nat) = Foo1 (Div a b) (1 <=? b)

type family Foo1 (r :: Nat) (valid :: Bool) :: Nat where
  Foo1 r 'True = r
  Foo1 _ 'False = TypeError ('Text "Oops, divide by zero")


f :: (KnownNat a, KnownNat b, r ~ (Foo a b)) => SNat a -> SNat b -> SNat r
f _ b = case ((SNat @1) %<= b) %~ STrue of
          (Proved k)  -> g b SNat
          (Disproved k) -> undefined

g :: (KnownNat b, 1 <= b) => SNat  b -> SNat r -> SNat r
g _ x = x

So you are saying that GHC should know that 1 <= b holds because if it didn't then your TypeError would be triggered? — luqui
@luqui I'm not saying GHC "should" now. I'm saying I want to tell GHC this holds. I understand that it's intractable for GHC to know such things generally. — CryptoNoob
Oh, you want to figure out a definition for f that will pass with the given signature? I do think you'll have to rephrase Foo1 or add an auxiliary family that describes the property -- I don't think it can be proven the way Foo1 is currently presented. (Because a type error is fatal AFAIK, you can't keep reasoning after you hit it) — luqui
@luqui I have experimented a little bit with the singletons library, see my edit. I want to make this work without having to change the type signatures of f and g. I think this should be possible using the singletons library. — CryptoNoob

Li-yao Xia Li-yao Xia · Accepted Answer · 2020-03-19T14:11:50

Here's a version of your snippet using singletons that compiles.

Use (TypeLits.%<=?), not (Ord.%<=). (See also haddocks for (%<=?) for more details).
Use sDiv to construct the singleton value for Div a b from a and b. SNat requires an extra KnownNat r constraint that would make the whole thing redundant.

{-# LANGUAGE
   EmptyCase,
    DataKinds,
    TypeFamilies,
    KindSignatures,
    TypeApplications,
    TypeOperators,
    UndecidableInstances #-}

module Test where

import Data.Proxy
import GHC.TypeLits
import Data.Bool
import GHC.Err

import Data.Singletons.TypeLits ( Sing (SNat), SNat, (%<=?), sDiv)
import Data.Singletons.Decide
import Data.Singletons.Prelude.Bool
import Data.Kind (Type)

type Foo (a :: Nat) (b :: Nat) = Foo1 (Div a b) (1 <=? b)

type family Foo1 (r :: Nat) (valid :: Bool) :: Nat where
  Foo1 r 'True = r
  Foo1 _ 'False = TypeError ('Text "Oops, divide by zero")

f :: (KnownNat a, KnownNat b, r ~ Foo a b) => SNat a -> SNat b -> SNat r
f a b = case (SNat @1) %<=? b of
          STrue -> g b (sDiv a b)
          SFalse -> undefined

g :: (KnownNat b, 1 <= b) => SNat  b -> SNat r -> SNat r
g _ x = x

Proof a constraint when using a type family

1 Answers