<div dir="ltr"><div dir="ltr"><div dir="ltr"><div>Hi Everyone, <br></div><div>I tried to come up with a solution, but it has plenty of drawbacks. <br></div><div><br></div><div><br>data Tag = Hdf5 | Cbf | Unchecked<br><br>data A :: Tag -> Type where<br>  Ca :: Symbol -> A Unchecked<br>  Ch :: A Hdf5<br>  Cb :: A Cbf<br><br>type family Typestring (a :: A Unchecked) :: Type<br>type instance Typestring (Ca "hdf5") = A Hdf5<br>type instance Typestring (Ca "cbf") = A Cbf<br><br>data SUnchecked a where<br>  Sh :: SUnchecked (Ca "hdf5")<br>  Sc :: SUnchecked (Ca "cbf")<br><br></div><div>This checkValue function is useless, because you need to pass A Unchecked, and constructor (Ca) takes Symbol rather than String,  and value of type SUnchecked a. <br>checkValue :: forall (a :: A Unchecked). A Unchecked ->  SUnchecked a -> Typestring a<br>checkValue  (Ca x) Sh = Ch<br>checkValue  (Ca x) Sc = Cb</div><div><br></div><div>When I tried to run the above code <br></div><div>*Main> :t checkValue (Ca (someSymbolVal "hdf5")) <br><br><interactive>:1:17: error:<br>    • Couldn't match expected type ‘Symbol’<br>                  with actual type ‘GHC.TypeLits.SomeSymbol’<br>    • In the first argument of ‘Ca’, namely ‘(someSymbolVal "hdf5")’<br>      In the first argument of ‘checkValue’, namely<br>        ‘(Ca (someSymbolVal "hdf5"))’<br>      In the expression: checkValue (Ca (someSymbolVal "hdf5"))<br></div><div><br></div><div><br></div><div> What I really want is something like this, but the problem is I can't do pattern matching on symbols, and if I change 
the data type to String from Symbol then it won't compile . <br></div><div>Could some one point me how to solve this problem? <br></div><div><br></div><div> checkValue :: forall (a :: A Unchecked). SUnchecked a => A Unchecked -> Typestring a<br> checkValue (Ca "hdf5") = Ch<br> checkValue (Ca "cbf") = Cb <br><br></div><div>Best regards,</div><div>Mukesh <br></div><div><br><br><br></div></div></div></div><br><div class="gmail_quote"><div dir="ltr">On Thu, Oct 4, 2018 at 11:11 PM Francesco Ariis <<a href="mailto:fa-ml@ariis.it">fa-ml@ariis.it</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello Nikita,<br>
<br>
On Thu, Oct 04, 2018 at 02:50:09AM +0300, Никита Фуфаев wrote:<br>
> As this problem requires type to depend on runtime value,<br>
> you need singletons.<br>
<br>
Many thanks for showing us the way, very elegant solution.<br>
_______________________________________________<br>
Beginners mailing list<br>
<a href="mailto:Beginners@haskell.org" target="_blank">Beginners@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners</a><br>
</blockquote></div>