title: Specifying a dependent type via type family in a GADT data constructor
body: <p>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 <code>ComplexThing</code> type, which is a GADT parameterized by a much simpler type, <code>MyEnum</code>. There are many constructors of <code>ComplexThing</code>, though, that are only valid when applied to certain (possibly many) members of <code>MyEnum</code>.</p>
  
  <p>One way to address this problem is to break these constructors into simpler variants. Below I have one such constructor, <code>NotSimple</code>, which might be recast as <code>NotSimple_B</code> or <code>NotSimple_C</code>. In general this seems like a less elegant solution.</p>
  
  <p>What I would prefer is that the user of this type should be able to write something like <code>NotSimple ThingB</code> or <code>NotSimple ThingC</code>, and that <code>NotSimple ThingA</code> should not type check. For the purposes of defining <code>ComplexThing</code>, I also want the specification of the allowable subset of <code>MyEnum</code> 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 <code>SMyEnum</code>.</p>
  
  <p>I've come pretty close to getting what I want. I can actually use what I've set up, but full <em>usability</em> isn't there. In particular, writing <code>NotSimple SThingB</code> 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.</p>
  
  <p>See my implementation below, along with a few tests and their results.</p>
  
  <pre class="lang-hs prettyprint-override"><code>{-# 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)] -&gt; Type where
    Simple :: ComplexThing [ '(ThingA, ThingA), '(ThingA, ThingB), '(ThingC, ThingB) ]
    NotSimple :: forall x. MyEnumChoice '[ ThingB, ThingC ] x -&gt; 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)]
  </code></pre>
  
  <p>I think I understand the <em>why</em> behind this type checking failure. My hope was that <code>x0</code> could be magically unified with the argument to <code>NotSimple</code>, 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, <code>SThingB</code>) 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.</p>
  
  <p>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.</p>