title: Static Guarantee on Key/Value Relationships in Data.Map
body: <p>I want to make a special smart constructor for Data.Map with a certain constraint on the types of key/value pair relationships. This is the constraint I tried to express:</p>
  
  <pre><code>{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DataKinds #-}
  
  data Field = Speed | Name | ID
  data Value = VFloat Float | VString ByteString | VInt Int
  
  class Pair f b | f -&gt; b where
      toPair :: f -&gt; b -&gt; (f, b)
      toPair = (,)
  
  instance Pair Speed (VFloat f) 
  instance Pair ID (VInt i)
  </code></pre>
  
  <p>for each field, there is only one type of value that it should be associated with. In my case, it does not make sense for a <code>Speed</code> field to map to a <code>ByteString</code>. A <code>Speed</code> field should uniquely map to a <code>Float</code></p>
  
  <p>But I get the following type error:</p>
  
  <pre><code>Kind mis-match
  The first argument of `Pair' should have kind `*',
  but `VInt' has kind `Value'
  In the instance declaration for `Pair Speed (VFloat f)'
  </code></pre>
  
  <p>using <code>-XKindSignatures</code>:</p>
  
  <pre><code>class Pair (f :: Field) (b :: Value) | f -&gt; b where
      toPair :: f -&gt; b -&gt; (f, b)
      toPair = (,)
  
  Kind mis-match
  Expected kind `OpenKind', but `f' has kind `Field'
  In the type `f -&gt; b -&gt; (f, b)'
  In the class declaration for `Pair'
  </code></pre>
  
  <p>I understand why I get the Kind mis-match, but how can I express this constraint so that it is a compile time type-checker error to use <code>toPair</code> on an non-matching <code>Field</code> and <code>Value</code>.</p>
  
  <p>It was suggested to me by #haskell to use a <code>GADT</code>, but I havent been able to figure it out yet.</p>
  
  <p>The goal of this is to be able to write</p>
  
  <pre><code>type Record = Map Field Value
  
  mkRecord :: [Field] -&gt; [Value] -&gt; Record
  mkRecord = (fromList .) . zipWith toPair
  </code></pre>
  
  <p>so that I can make safe <code>Map</code>s where the key/value invariants are respected.</p>
  
  <p>So this should type-check</p>
  
  <pre><code>test1 = mkRecord [Speed, ID] [VFloat 1.0, VInt 2]
  </code></pre>
  
  <p>but this should be a compile time error</p>
  
  <pre><code>test2 = mkRecord [Speed] [VInt 1]
  </code></pre>
  
  <p>EDIT:</p>
  
  <p>I'm beginning to think that my specific requirements aren't possible. Using my original example</p>
  
  <pre><code>data Foo = FooInt | FooFloat
  data Bar = BarInt Int | BarFloat Float
  </code></pre>
  
  <p>In order to enforce the constraint on <code>Foo</code> and <code>Bar</code>, there must be some way to differentiate between a <code>FooInt</code> and <code>FooFloat</code> at the type level and similarly for <code>Bar</code>. Thus I instead need two GADTs</p>
  
  <pre><code>data Foo :: * -&gt; * where
      FooInt   :: Foo Int
      FooFloat :: Foo Float
  
  data Bar :: * -&gt; * where
      BarInt   :: Int   -&gt; Bar Int
      BarFloat :: Float -&gt; Bar Float
  </code></pre>
  
  <p>now I can write an instance for <code>Pair</code> that only holds when the <code>Foo</code> and <code>Bar</code> are both tagged with the same type</p>
  
  <pre><code>instance Pair (Foo a) (Bar a)
  </code></pre>
  
  <p>and I have the properties I want</p>
  
  <pre><code>test1 = toPair FooInt (BarInt 1)   -- type-checks
  test2 = toPair FooInt (BarFloat 1) -- no instance for Pair (Foo Int) (Bar Float)
  </code></pre>
  
  <p>but I lose the ability to write <code>xs = [FooInt, FooFloat]</code> because that would require a heterogeneous list. Furthermore if I try to make the <code>Map</code> synonym <code>type FooBar = Map (Foo ?) (Bar ?)</code> I'm stuck with a <code>Map</code> of either only <code>Int</code> types or only <code>Float</code> types, which isnt what I want. It's looking rather hopeless, unless theres some powerful type class wizardry I'm not aware of.</p>