<div dir="ltr">The type `a` only appears in the constraints, not the signature, so GHC has no way of figuring out what it's supposed to be. Furthermore, the type `a` in your signature is *not* the type `a` that's in the GADT -- that's a totally distinct type. I don't think you'll be able to unify the those two types.<div><br></div><div>You can use a `Proxy` argument to explicitly signal to GHC what type it should be, or TypeApplications, but I don't think either of those will help with implementing this.</div><div><br></div><div>You may also find <a href="http://haddock.stackage.org/lts-5.1/constraints-0.8/Data-Constraint.html">http://haddock.stackage.org/lts-5.1/constraints-0.8/Data-Constraint.html</a> interesting.</div></div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div>Matt Parsons</div></div></div></div>
<br><div class="gmail_quote">On Thu, May 4, 2017 at 9:55 PM, MarLinn <span dir="ltr"><<a href="mailto:monkleyon@gmail.com" target="_blank">monkleyon@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
  

    
  
  <div text="#000000" bgcolor="#FFFFFF">
    <p>Hi,</p>
    <p>I've been working on a kind of constrained version of
      Data.Dynamic:</p>
    <pre> data Dynamic (c :: * -> Constraint) where
            Dynamic :: (Typeable a, c a) => a -> Dynamic c
</pre>
    <p>The idea is that Data.Dynamic gives up all compile time type
      information. In this variant I can at least keep a bit of the
      information around that I have. (In fact I can even "lift" a type
      into a constraint, thereby keeping <i>all</i> information.) Most
      of my functions are nailed down, including mappings and
      traversals. But one group of functions eludes me: functions to
      change only the constraint, while keeping the value. Here is one
      of my goal types:</p>
    <pre> castDynamic :: ( Typeable a, c a, d a ) => Dynamic c -> Dynamic d
</pre>
    <p>I'm pretty sure I'll have to sprinkle in a <tt>Proxy a</tt>, but
      so be it. I've thrown all typing tricks at this function that I
      know of, from unsafeCoerce over case-of instead of pattern
      matching, to ScopedTypeVariables. But I couldn't convince ghci to
      accept my code. So I tried something simpler.</p>
    <pre> castDynamic' :: (Typeable a, c a) => Dynamic Show -> Maybe (Dynamic c)
</pre>
    <p>Here's where it gets funny: I can implement this function in ghci
      interactively just fine.</p>
    <pre> >>> :t \(d :: Dynamic Show) -> case d of Dynamic a -> Dynamic <$> cast a
        \(d :: Dynamic Show) -> case d of Dynamic a -> Dynamic <$> cast a
          :: (Typeable a, c a) => Dynamic Show -> Maybe (Dynamic c)
</pre>
    <p>But when I enter the exact same code in a file and load it, ghci
      balks at me because <tt>a</tt> is too ambiguous. Again, I've
      tried if it's the monomorphism restriction, or if I need to
      sprinkle in more (scoped) signatures or explicit <tt>forall</tt>'s
      etc… nothing helped.</p>
    <p>What is the difference here? Am I missing an extension? Am I
      doing something I shouldn't and the interactive mode is just doing
      me a favor? There was a discussion on this list less than a month
      ago where it was mentioned that ghci handles polymorphic types
      differently depending on the source of the code. Is there some
      documentation on these differences? Any help would be appreciated.<br>
    </p>
    <p>Cheers,<br>
      MarLinn<br>
    </p>
  </div>

<br>______________________________<wbr>_________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/haskell-<wbr>cafe</a><br>
Only members subscribed via the mailman list are allowed to post.<br></blockquote></div><br></div>