Fwd: constraint inference

Sorry, I didn't copy to cafe...
---------- Forwarded message ----------
From: Dmitry Olshansky
You've specified RankNTypes but aren't using it; did you mean "(forall n. KnownSymbol n => Proxy n)" ?
Typically in these situations you also can't partially apply it, so you might need to make it "f p = symbolVal p".
On 7 July 2017 at 15:50, Dmitry Olshansky
wrote: Hello, cafe!
If we have many constraints then compiling is sometimes too slow. Especially if there are some type calculations. And I don't know how to divide this time among different source files because all constraints are checked only when we call a function.
I tried to add constraint info into argument definition instead of the function signature but this trick is not working (see below).
Is it (at least theoretically) possible to infer the constraint inside a function from the type of function's argument?
------------------------------------ $ stack ghci ---- GHCi, version 8.0.2: Prelude> import Data.Proxy Prelude Data.Proxy> import GHC.TypeLits Prelude Data.Proxy GHC.TypeLits> :set -XRankNTypes Prelude Data.Proxy GHC.TypeLits> let { f :: (KnownSymbol n => Proxy n) -> String; f = symbolVal }
<interactive>:4:54: error: • No instance for (KnownSymbol n) arising from a use of ‘symbolVal’ Possible fix: add (KnownSymbol n) to the context of the type signature for: f :: (KnownSymbol n => Proxy n) -> String • In the expression: symbolVal In an equation for ‘f’: f = symbolVal ------------------------------------
Best regards, Dmitry
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
-- Ivan Lazar Miljenovic Ivan.Miljenovic@gmail.com http://IvanMiljenovic.wordpress.com

On 07/07/2017 02:50 AM, Dmitry Olshansky wrote:
I am not sure why but when I didn't set RankNTypes I got an appropriate error. So I specified it.
But if I write let { f :: (forall n. KnownSymbol n => Proxy n) -> String; f p = symbolVal p } then nothing is changed.
What would the String (f Proxy) be? (Note that (Proxy :: forall n. KnownSymbol n => Proxy n) would be a valid argument here.)

You are right, thanks!
2017-07-07 22:17 GMT+03:00 Li-yao Xia
On 07/07/2017 02:50 AM, Dmitry Olshansky wrote:
I am not sure why but when I didn't set RankNTypes I got an appropriate error. So I specified it.
But if I write let { f :: (forall n. KnownSymbol n => Proxy n) -> String; f p = symbolVal p } then nothing is changed.
What would the String (f Proxy) be? (Note that (Proxy :: forall n. KnownSymbol n => Proxy n) would be a valid argument here.)
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
participants (2)
-
Dmitry Olshansky
-
Li-yao Xia