How to convince GHC about type equality on a recursive type

Question

I'm defining a type whose type parameters have some relations. I have Item type which takes Cat and SubCat, but you can use some of the types of SubCat depending on Cat. For example, when you specify Cat1 as Cat, you can specify SubCat1 or SubCat2 as SubCat.

I implemented it using ValidSubCats type family to define valid SubCats for each Cat, and OneOf type family to define a constraint.

{-# LANGUAGE DataKinds, GADTs, PolyKinds, StandaloneKindSignatures, TypeFamilies, TypeOperators #-}

import Data.Kind (Constraint, Type)
import Data.Type.Equality ((:~:)(..), TestEquality(..))
import Unsafe.Coerce (unsafeCoerce)

data Cat = Cat1 | Cat2
type SCat :: Cat -> Type
data SCat cat where
    SCat1 :: SCat 'Cat1
    SCat2 :: SCat 'Cat2

data SubCat = SubCat1 | SubCat2 | SubCat3
type SSubCat :: SubCat -> Type
data SSubCat subCat where
    SSubCat1 :: SSubCat 'SubCat1
    SSubCat2 :: SSubCat 'SubCat2
    SSubCat3 :: SSubCat 'SubCat3

type ValidSubCats :: Cat -> [SubCat]
type family ValidSubCats cat where
    ValidSubCats 'Cat1 = '[ 'SubCat1, 'SubCat2 ]
    ValidSubCats 'Cat2 = '[ 'SubCat2, 'SubCat3 ]

type OneOf :: k -> [k] -> Constraint
type family OneOf t ts where
    OneOf t (t ': _) = ()
    OneOf t (_ ': ts) = OneOf t ts
    OneOf _ _ = ('True ~ 'False)

type Item :: Cat -> SubCat -> Type
data Item cat subCat where
    Item :: OneOf subCat (ValidSubCats cat) => Item cat subCat

Now, I'm trying to define a function to create an Item from SCat and SSubCat.

type HL :: (k -> Type) -> [k] -> Type
data HL f t where
    HCons :: f t -> HL f ts -> HL f (t ': ts)
    HNil :: HL f '[]
infixr 5 `HCons`

validSSubCats :: SCat cat -> HL SSubCat (ValidSubCats cat)
validSSubCats SCat1 = SSubCat1 `HCons` SSubCat2 `HCons` HNil
validSSubCats SCat2 = SSubCat2 `HCons` SSubCat3 `HCons` HNil

instance TestEquality SSubCat where
    testEquality SSubCat1 SSubCat1 = Just Refl
    testEquality SSubCat2 SSubCat2 = Just Refl
    testEquality SSubCat3 SSubCat3 = Just Refl
    testEquality _ _ = Nothing

oneOf :: TestEquality f => f t -> HL f ts -> Maybe (OneOf t ts :~: (() :: Constraint))
oneOf x (HCons y ys) = case testEquality x y of
                           Just Refl -> Just Refl
                           Nothing -> unsafeCoerce $ oneOf x ys
oneOf _ HNil = Nothing

makeItem :: SCat cat -> SSubCat subCat -> Maybe (Item cat subCat)
makeItem sCat sSubCat = case oneOf sSubCat (validSSubCats sCat) of
                            Just Refl -> Just Item
                            Nothing -> Nothing

But as you can see, I'm using unsafeCoerce to define oneOf. I got this error when I removed it.

test.hs:54:39: error:
    • Could not deduce: OneOf t ts1 ~ OneOf t (t1 : ts1)
      from the context: ts ~ (t1 : ts1)
        bound by a pattern with constructor:
                   HCons :: forall {k} (f :: k -> *) (t :: k) (ts :: [k]).
                            f t -> HL f ts -> HL f (t : ts),
                 in an equation for ‘oneOf’
        at q.hs:52:10-19
      Expected: Maybe (OneOf t ts :~: (() :: Constraint))
        Actual: Maybe (OneOf t ts1 :~: (() :: Constraint))
      NB: ‘OneOf’ is a non-injective type family
    • In the expression: oneOf x ys
      In a case alternative: Nothing -> oneOf x ys
      In the expression:
        case testEquality x y of
          Just Refl -> Just Refl
          Nothing -> oneOf x ys
    • Relevant bindings include
        ys :: HL f ts1 (bound at q.hs:52:18)
        y :: f t1 (bound at q.hs:52:16)
        x :: f t (bound at q.hs:52:7)
        oneOf :: f t
                 -> HL f ts -> Maybe (OneOf t ts :~: (() :: Constraint))
          (bound at q.hs:52:1)
   |
54 |                            Nothing -> oneOf x ys
   |                                       ^^^^^^^^^^

How can I convince GHC that it can infer OneOf t (t ': ts) :~: (() :: Constraint) from OneOf t ts :~: (() :: Constraint) without using unsafeCoerce?

Answer 1

I would suggest using something which has a value-level representation, since we can directly manipulate such things more easily. This is often easier to work with in general. For example:

data OneOf' t ts where
  Here :: forall t ts. OneOf' t (t ': ts)
  There :: forall t t2 ts. OneOf' t ts -> OneOf' t (t2 ': ts)

oneOf' :: TestEquality f => f t -> HL f ts -> Maybe (OneOf' t ts)
oneOf' _ HNil = Nothing
oneOf' x (HCons y ys) =
  case testEquality x y of
    Just Refl -> Just Here
    Nothing -> There <$> oneOf' x ys

This does not directly answer the question as asked, although if you can write a function with type

convertOneOf :: forall t ts. OneOf' t ts -> (OneOf t ts :~: (() :: Constraint))

then it would answer the exact question. Right now, I'm not sure how to do this (or even whether it is possible). I think you need an auxiliary function

weakenOneOf :: forall t t2 ts. OneOfTrue t ts -> OneOfTrue t (t2 ': ts)

(where I've used the synonym OneOfTrue to make things easier to read: type OneOfTrue t ts = OneOf t ts :~: (() :: Constraint)).

If this can be implemented then you should be good to go, although I would probably still prefer to use OneOf' when possible.

It's worth noting that something like OneOf' is a relatively common construct in dependently typed languages: There's an Agda example here, an Idris example here and a similar thing in Coq here. Each of these has value-level content in the same way that OneOf' does.

Item could be rewritten to use OneOf' like this:

type Item' :: Cat -> SubCat -> Type
data Item' cat subCat where
    Item' :: OneOf' subCat (ValidSubCats cat) -> Item' cat subCat

and there is a corresponding rewrite for makeItem to use Item'.

Why the original OneOf is tricky and OneOf' is less tricky

It is often difficult to work with something like OneOf. One reason is that Haskell allows type families which can get "stuck". This prevents can prevent some type-level "reductions" and we do not have things like canonical forms.

For example, consider this definition which could be useful in dealing with something like type-level lists passed to a OneOf:

listDecideNilCons :: forall ts. Either (ts :~: '[]) (IsCons ts)
listDecideNilCons = ...

data IsCons a where
  MkIsCons :: forall t ts. IsCons (t ': ts)

listDecideNilCons would just tell you that a type-level list is either a nil or a cons, which seems pretty reasonable and it would be a handy fact to make use of. In fact, I suspect that it would be necessary to be able to implement listDecideNilCons or something similar to it in order to be able to implement convertOneOf. I suspect even more strongly that it is necessary to implement the other direction of the conversion.

However, the existence of stuck type families is sufficient to show that listDecideNilCons cannot be implemented. Consider:

type family Sticky (b :: Bool) :: [Int] where
  Sticky True = '[]

example :: Either ((Sticky False) :~: '[]) (IsCons (Sticky False))
example = listDecideNilCons

This code type-checks. What should the value of example be? Since Sticky False cannot be reduced any further, there isn't a value for example that would make sense.

Note that if we also have value-level information, like we do with OneOf', we do not run into this issue for two reasons: Stuck types are not an issue because we can control which specific "shapes" (like '[] and ... ': ...) we are allowed to take in and we can use the proof values when we construct proofs of new things.

For example, in the case of OneOf', it ensures that the type-level list will have the "shape" ... ': .... In the function oneOf', we are using the proof value from the recursive call oneOf' x ys to build a larger proof.

In the original oneOf function, we cannot make use of the fact that the result of a recursive call will either have a "cons shape" or it will give back Nothing (since the original OneOf doesn't give us this information). However, we must know this to use the result of the recursive call to produce the desired result since the original OneOf requires a "cons shape".