<div dir="ltr">To explain, you should think of<div><br></div><div>forall (k :: FileKind) . Entry k</div><div><br></div><div>as being different than</div><div><br></div><div>Entry 'FOLDER</div><div>Entry 'FILE</div><div><br></div><div>The difference being that anything that is 'k' must be able to satisfy all FileKind not just one of them.</div><div><br></div><div>James</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Nov 12, 2014 at 11:47 PM, James M <span dir="ltr"><<a href="mailto:jmartin@eecs.berkeley.edu" target="_blank">jmartin@eecs.berkeley.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">This is easily testable.<div><div><br></div><div>deriving instance Typeable Entry</div><div>deriving instance Typeable FileKind<br></div><div>deriving instance Typeable 'FOLDER</div><div>deriving instance Typeable 'FILE</div></div><div><br></div><div><div>convertBack :: SomeEntry -> Either (Entry FILE) (Entry FOLDER)</div><div>convertBack (SomeEntry x)</div><div>    | typeOf x == typeOf (Folder "" "") = Right x</div><div>    | otherwise = Left x</div></div><div><br></div><div>The error I get is this:</div><div><br></div><div><div>    Couldn't match type ‘k’ with ‘'FOLDER’</div><div>      ‘k’ is a rigid type variable bound by</div><div>          a pattern with constructor</div><div>            SomeEntry :: forall (k :: FileKind). Entry k -> SomeEntry,</div><div>          in an equation for ‘convertBack’</div><div>          at cafe2.hs:24:14</div><div>    Expected type: Entry 'FOLDER</div><div>      Actual type: Entry k</div><div>    Relevant bindings include x :: Entry k (bound at cafe2.hs:24:24)</div><div>    In the first argument of ‘Right’, namely ‘x’</div><div>    In the expression: Right x</div></div><span class="HOEnZb"><font color="#888888"><div><br></div><div>James</div><div><br></div></font></span></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Nov 12, 2014 at 11:29 PM, Bardur Arantsson <span dir="ltr"><<a href="mailto:spam@scientician.net" target="_blank">spam@scientician.net</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span>On 2014-11-13 08:10, James M wrote:<br>
> I didn't explain Frank's case, only the one I constructed.<br>
><br>
> convertBack :: SomeEntry -> Either (FsEntry FILE) (FsEntry FOLDER)<br>
><br>
> For this function to work, we would need some way to inspect the type as a<br>
> value, and this can only generally be done with dependent types.<br>
><br>
> convertBack :: SomeEntry -> FsEntry k<br>
><br>
> This case is technically possible to do statically, but not very useful<br>
> because we have no idea what the actual type is. Therefore, we could only<br>
> use it on things that work for all FsEntry and not just a subset.<br>
><br>
> We could ask for what 'k' is in the type system and perform the necessary<br>
> computation in the type system. However, this is complicated, and Haskell<br>
> currently only has very limited support for moving between values and<br>
> types. You can look at GHC.TypeLits for an example of this.<br>
<br>
</span>Maybe I'm missing something, but wouldn't adding a Typeable constraint<br>
on the existential give you the option of casting back? AFAICT that<br>
should be sufficient since the FileKind is closed and you can thus just<br>
attempt both conversions and see which one succeeds.<br>
<br>
Regards,<br>
<div><div><br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>