Specifying a dependent type via type family in a GADT data constructor

Question

I've been trying to implement what seems to be a fairly straightforward type. Below is a contrived example that demonstrates the problem. At the core of it, I want to implement some ComplexThing type, which is a GADT parameterized by a much simpler type, MyEnum. There are many constructors of ComplexThing, though, that are only valid when applied to certain (possibly many) members of MyEnum.

One way to address this problem is to break these constructors into simpler variants. Below I have one such constructor, NotSimple, which might be recast as NotSimple_B or NotSimple_C. In general this seems like a less elegant solution.

What I would prefer is that the user of this type should be able to write something like NotSimple ThingB or NotSimple ThingC, and that NotSimple ThingA should not type check. For the purposes of defining ComplexThing, I also want the specification of the allowable subset of MyEnum to be fairly general (i.e. it should be OK to repeat elements in the specification, order should not matter, and it should be flexible in terms of the number of allowed elements). For this reason I've pursued the use of a type-level list, and a type family that walks that list, with the help of a singleton type SMyEnum.

I've come pretty close to getting what I want. I can actually use what I've set up, but full usability isn't there. In particular, writing NotSimple SThingB by itself is too much for the type checker. With the appropriate type signatures, it becomes tenable, but my view is that this is too much of a burden to put on potential users.

See my implementation below, along with a few tests and their results.

{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE PartialTypeSignatures     #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE TypeOperators             #-}

import Data.Kind (Type)

data MyEnum = ThingA
            | ThingB
            | ThingC
            | ThingD

data family SMyEnum (e :: MyEnum)
data instance SMyEnum ThingA = SThingA
data instance SMyEnum ThingB = SThingB
data instance SMyEnum ThingC = SThingC
data instance SMyEnum ThingD = SThingD

type family MyEnumChoice (l :: [MyEnum]) (e :: MyEnum) :: Type where
  MyEnumChoice (e ': ls) e = SMyEnum e
  MyEnumChoice (f ': ls) e = MyEnumChoice ls e

data ComplexThing :: [(MyEnum,MyEnum)] -> Type where
  Simple :: ComplexThing [ '(ThingA, ThingA), '(ThingA, ThingB), '(ThingC, ThingB) ]
  NotSimple :: forall x. MyEnumChoice '[ ThingB, ThingC ] x -> ComplexThing '[ '(ThingA, x), '(x, ThingD) ]

test3 :: ComplexThing '[ '(ThingA, ThingB), '(ThingB, ThingD) ]
test3 = NotSimple SThingB
-- Checks!

test3_2 :: ComplexThing '[ '(_, ThingB), _]
test3_2 = NotSimple SThingB
-- Checks!

test4 = NotSimple SThingB
-- • Couldn't match expected type ‘MyEnumChoice
--                                   '[ 'ThingB, 'ThingC] x0’
--               with actual type ‘SMyEnum 'ThingB’
--   The type variable ‘x0’ is ambiguous
-- • In the first argument of ‘NotSimple’, namely ‘SThingB’
--   In the expression: NotSimple SThingB
--   In an equation for ‘test4’: test4 = NotSimple SThingB
-- • Relevant bindings include
--     test4 :: ComplexThing '[ '( 'ThingA, x0), '(x0, 'ThingD)]

I think I understand the why behind this type checking failure. My hope was that x0 could be magically unified with the argument to NotSimple, but what the type checker sees instead is that it must unify the final type that would be produced by that type family (the argument, SThingB) with the general, universally-quantified specification of that constructor's argument. I'm not sure, however, what the best way to work around this limitation is.

Any suggestions as to how I might approach this are appreciated! If I've demonstrated any conceptual or terminological misunderstandings, commentary on that is welcome as well.

Answer 1

I substituted your Type

type family MyEnumChoice (l :: [MyEnum]) (e :: MyEnum) :: Type

with a Constraint

type family MyEnumCheck (l :: [MyEnum]) (e :: MyEnum) :: Constraint where

to check membership, and adapted your GADT accordingly. I don't know if this is general enough for you, but it might be a starting point.

{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE PartialTypeSignatures     #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE TypeOperators             #-}

import Data.Kind (Type, Constraint)

data MyEnum = ThingA
            | ThingB
            | ThingC
            | ThingD

data family SMyEnum (e :: MyEnum)
data instance SMyEnum ThingA = SThingA
data instance SMyEnum ThingB = SThingB
data instance SMyEnum ThingC = SThingC
data instance SMyEnum ThingD = SThingD

type family MyEnumCheck (l :: [MyEnum]) (e :: MyEnum) :: Constraint where
  MyEnumCheck (e ': ls) e = ()
  MyEnumCheck (f ': ls) e = MyEnumCheck ls e

data ComplexThing :: [(MyEnum,MyEnum)] -> Type where
  Simple :: ComplexThing [ '(ThingA, ThingA), '(ThingA, ThingB), '(ThingC, ThingB) ]
  NotSimple :: forall x. MyEnumCheck '[ ThingB, ThingC ] x => 
     SMyEnum x -> ComplexThing '[ '(ThingA, x), '(x, ThingD) ]

test3 :: ComplexThing '[ '(ThingA, ThingB), '(ThingB, ThingD) ]
test3 = NotSimple SThingB
-- Checks!

test3_2 :: ComplexThing '[ '(_, ThingB), _]
test3_2 = NotSimple SThingB
-- Checks!

test4 = NotSimple SThingB
-- Checks!