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?
CodePudding user response：
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".