GADT with Type level Bool - making (&&) type operator imply constraints for its arguments-CodePudding

In summary I am trying to understand how I can tell ghc that a && b ~ True should imply that a ~ True and b ~ True within the context of a GADT.

Given a data constructor:

data Foo :: Bool -> * where
    ...
    Bar :: Foo j -> Foo k -> Foo (j && k)
    ...

and, as an example, an instance for Eq (Foo True):

instance Eq (Foo True) where
   (Bar foo11 foo12) == (Bar foo21 foo22) = foo11 == ff21 && foo12 == foo22
   ....

the compiler gives the following error:

Could not deduce: k1 ~ k
      from the context: 'True ~ (j && k)
        bound by a pattern with constructor:
                   Bar :: forall (j :: Bool) (k :: Bool).
                          Foo j -> Foo k -> Foo (j && k),
                 in an equation for `=='
        at Main.hs:12:4-14
      or from: 'True ~ (j1 && k1)
        bound by a pattern with constructor:
                   Bar :: forall (j :: Bool) (k :: Bool).
                          Foo j -> Foo k -> Foo (j && k),
                 in an equation for `=='
        at Main.hs:12:21-31
      `k1' is a rigid type variable bound by
        a pattern with constructor:
          Bar :: forall (j :: Bool) (k :: Bool).
                 Foo j -> Foo k -> Foo (j && k),
        in an equation for `=='
        at Main.hs:12:21-31
      `k' is a rigid type variable bound by
        a pattern with constructor:
          Bar :: forall (j :: Bool) (k :: Bool).
                 Foo j -> Foo k -> Foo (j && k),
        in an equation for `=='
        at Main.hs:12:4-14
      Expected type: Foo k
        Actual type: Foo k1
    * In the second argument of `(==)', namely `f22'
      In the second argument of `(&&)', namely `f12 == f22'
      In the expression: f11 == f21 && f12 == f22
    * Relevant bindings include
        f22 :: Foo k1 (bound at Main.hs:12:29)
        f12 :: Foo k (bound at Main.hs:12:12)

(and an equivalent error for j and j1)

This is obviously complaining that it doesn't know that f12 :: Foo k and f22 :: Foo k1 have the same type.

Recently I have been using typelit-nat-normalise to solve what felt like a similar issue (with typenat addition), and I have searched for a similar library that may resolve these issues for bools - but to no avail.

I have found typelevel-rewrite-rules, which I think might enable me to write some kind of rewrite rule for this but I can't work out the syntax for telling the compiler that:

(a && b ~ True) implies (a ~ True) AND (b ~ True). Which I believe would solve this issue.

CodePudding user response：

I believe that such kind of "inversion" of a type family is impossible in current GHC, at least without unsafe functions.

Even with unsafe functions, I don't know if it is safe to add it. Kinds are weird beasts, and often contain more terms than one would expect. E.g. type family X :: Bool compiles, still we can not prove X ~ 'True nor X ~ 'False.

The code below does not fully answer the question, but I wanted to remark that, if we can add a few constraints to Foo so to carry a few singletons around, then we can write the wanted Eq instance.

The code below can probably be simplified further. Still, here it is. Below, I defined "conversion" functions fooT1, fooT2 to convince GHC that in Foo k and Foo j we do have k ~ j ~ 'True.

{-# LANGUAGE GADTs, ScopedTypeVariables, TypeApplications,
    DataKinds, TypeOperators, KindSignatures,
    FlexibleInstances, AllowAmbiguousTypes #-}
{-# OPTIONS -Wall #-}

import Data.Singletons
import Data.Singletons.Prelude.Bool

data Foo :: Bool -> * where
    Bar :: (SingI j, SingI k) =>
           Foo j -> Foo k -> Foo (j && k)

fooT1 :: forall a b. (SingI a, SingI b, (a && b) ~ 'True) 
      => Foo a -> Foo b -> Foo 'True
fooT1 f _ = case (sing @a, sing @b) of
   (STrue, STrue) -> f

fooT2 :: forall a b. (SingI a, SingI b, (a && b) ~ 'True)
      => Foo a -> Foo b -> Foo 'True
fooT2 _ f = case (sing @a, sing @b) of
   (STrue, STrue) -> f

instance Eq (Foo 'True) where
   (Bar foo11 foo12) == (Bar foo21 foo22) = 
      fooT1 foo11 foo12 == fooT1 foo21 foo22 &&
      fooT2 foo11 foo12 == fooT2 foo21 foo22

Note that the pattern match (STrue, STrue) is exhaustive, and no warnings are raised by GHC.