title: Confused about GADTs and propagating constraints
body: <p>There's plenty of Q&amp;A about <code>GADTs</code> being better than <code>DatatypeContexts</code>, because GADTs automagically make constraints available in the right places. For example <a href="https://stackoverflow.com/questions/24465586/why-constraints-on-data-are-a-bad-thing">here</a>, <a href="https://stackoverflow.com/questions/12770278/typeclass-constraints-on-data-declarations">here</a>, <a href="https://stackoverflow.com/questions/16927710/type-constraints-for-automatic-function-constraint-deduction-in-haskell">here</a>. But sometimes it seems I still need an explicit constraint. What's going on? Example adapted from <a href="https://stackoverflow.com/a/24466703/2840542">this answer</a>:</p>
  <pre><code>{-# LANGUAGE  GADTs  #-}
  import Data.Maybe                                              -- fromJust
  
  data GADTBag a  where
    MkGADTBag :: Eq a =&gt; { unGADTBag :: [a] } -&gt; GADTBag a
  
  baz (MkGADTBag x) (Just y) = x == y
  
  baz2           x        y  = unGADTBag x == fromJust y
  
  
  -- unGADTBag :: GADTBag a -&gt; [a]                               -- inferred, no Eq a
  
  -- baz ::          GADTBag a -&gt; Maybe [a] -&gt; Bool              -- inferred, no Eq a
  -- baz2 :: Eq a =&gt; GADTBag a -&gt; Maybe [a] -&gt; Bool              -- inferred, with Eq a
  </code></pre>
  <p>Why can't the type for <code>unGADTBag</code> tell us <code>Eq a</code>?</p>
  <p><code>baz</code> and <code>baz2</code> are morally equivalent, yet have different types. Presumably because <code>unGADTBag</code> has no <code>Eq a</code>, then the constraint can't propagate into any code using <code>unGADTBag</code>.</p>
  <p>But with <code>baz2</code> there's an <code>Eq a</code> constraint hiding inside the <code>GADTBag a</code>. Presumably <code>baz2</code>'s <code>Eq a</code> will want a duplicate of the dictionary already there(?)</p>
  <p>Is it that potentially a GADT might have many data constructors, each with different (or no) constraints? That's not the case here, or with typical examples for constrained data structures like Bags, Sets, Ordered Lists.</p>
  <p>The equivalent for a <code>GADTBag</code> datatype using <code>DatatypeContexts</code> infers <code>baz</code>'s type same as <code>baz2</code>.</p>
  <p>Bonus question: why can't I get an ordinary <code>... deriving (Eq)</code> for <code>GADTBag</code>? I can get one with <code>StandaloneDeriving</code>, but it's blimmin obvious, why can't GHC just do it for me?</p>
  <pre><code>deriving instance (Eq a) =&gt; Eq (GADTBag a)
  </code></pre>
  <p>Is the problem again that there might be other data constructors?</p>
  <p>(Code exercised at GHC 8.6.5, if that's relevant.)</p>
  <p><strong>Addit:</strong> in light of @chi's and @leftroundabout's answers -- neither of which I find convincing. All of these give <code>*** Exception: Prelude.undefined</code>:</p>
  <pre><code>*DTContexts&gt; unGADTBag undefined
  *DTContexts&gt; unGADTBag $ MkGADTBag undefined
  *DTContexts&gt; unGADTBag $ MkGADTBag (undefined :: String)
  *DTContexts&gt; unGADTBag $ MkGADTBag (undefined :: [a])
  
  *DTContexts&gt; baz undefined (Just &quot;hello&quot;)
  *DTContexts&gt; baz (MkGADTBag undefined) (Just &quot;hello&quot;)
  *DTContexts&gt; baz (MkGADTBag (undefined :: String)) (Just &quot;hello&quot;)
  
  *DTContexts&gt; baz2 undefined (Just &quot;hello&quot;)
  *DTContexts&gt; baz2 (MkGADTBag undefined) (Just &quot;hello&quot;)
  *DTContexts&gt; baz2 (MkGADTBag (undefined :: String)) (Just &quot;hello&quot;)
  </code></pre>
  <p>Whereas these two give the same type error at compile time <s><code>* Couldn't match expected type ``[Char]'</code></s><code>* No instance for (Eq (Int -&gt; Int)) arising from a use of ``MkGADTBag'</code>/<code> ``baz2'</code> respectively [<strong>Edit:</strong> my initial Addit gave the wrong expression and wrong error message]:</p>
  <pre><code>*DTContexts&gt; baz (MkGADTBag (undefined :: [Int -&gt; Int])) (Just [(+ 1)])
  *DTContexts&gt; baz2 (MkGADTBag (undefined :: [Int -&gt; Int])) (Just [(+ 1)])
  </code></pre>
  <p>So <code>baz, baz2</code> are morally equivalent not just in that they return the same result for the same well-defined arguments; but also in that they exhibit the same behaviour for the same ill-defined arguments. Or they differ only in where the absence of an <code>Eq</code> instance gets reported?</p>
  <blockquote>
  <p>@leftroundabout Before you've actually deconstructed the <code>x</code> value, there's no way of knowing that the <code>MkGADTBag</code> constructor indeed applies.</p>
  </blockquote>
  <p>Yes there is: field label <code>unGADTBag</code> is defined if and only if there's a pattern match on <code>MkGADTBag</code>. (It would maybe be different if there were other constructors for the type -- especially if those also had a label <code>unGADTBag</code>.) Again, being undefined/lazy evaluation doesn't postpone the type-inference.</p>
  <p>To be clear, by &quot;[not] convincing&quot; I mean: I can see the behaviour and the inferred types I'm getting. I don't see that laziness or potential undefinedness gets in the way of type inference. How could I expose a difference between <code>baz, baz2</code> that would explain why they have different types?</p>