Type error depending on scope of pattern matching
I'm curious if anyone can tell me why moving the pattern matching in these two examples makes it fail to compile, and what can be done to resolve the same issue in either of the latter two examples. As far as I can tell these should be equivalent. Unfortunately the solution used in the first examples won't work in the later ones due to the existential quantification. I've been asking on #haskell for a few days but haven't been able to find anyone who knows what the issue is. Code is available here: http://lpaste.net/137586 http://lpaste.net/137586 -- View this message in context: http://haskell.1045720.n5.nabble.com/Type-error-depending-on-scope-of-patter... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
You'll probably get more responses if you paste the code inline.
tom
El Aug 1, 2015, a las 11:25, htebalaka
I'm curious if anyone can tell me why moving the pattern matching in these two examples makes it fail to compile, and what can be done to resolve the same issue in either of the latter two examples. As far as I can tell these should be equivalent. Unfortunately the solution used in the first examples won't work in the later ones due to the existential quantification. I've been asking on #haskell for a few days but haven't been able to find anyone who knows what the issue is.
Code is available here: http://lpaste.net/137586 http://lpaste.net/137586
-- View this message in context: http://haskell.1045720.n5.nabble.com/Type-error-depending-on-scope-of-patter... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Alright. The first two examples show the issue and a fix for it; the last two have the same issue but existential quantification prevents the fix. grad has type "(Num a, Traversable t) => (forall s. Reifies s Tape => t (Reverse s a) -> Reverse s a) -> t a -> t a", and I'm basically trying to supply a function to it, either by being polymorphic over all Num (of which Reverse s a is an instance), or by providing the specific 'Reifies s Tape => ...' type, neither of which are working. amindfv wrote
You'll probably get more responses if you paste the code inline.
tom
El Aug 1, 2015, a las 11:25, htebalaka <
goodingm@
> escribió:
I'm curious if anyone can tell me why moving the pattern matching in these two examples makes it fail to compile, and what can be done to resolve the same issue in either of the latter two examples. As far as I can tell these should be equivalent. Unfortunately the solution used in the first examples won't work in the later ones due to the existential quantification. I've been asking on #haskell for a few days but haven't been able to find anyone who knows what the issue is.
Code is available here: http://lpaste.net/137586 <http://lpaste.net/137586>;
-- View this message in context: http://haskell.1045720.n5.nabble.com/Type-error-depending-on-scope-of-patter... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. _______________________________________________ Haskell-Cafe mailing list
Haskell-Cafe@
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Haskell-Cafe mailing list
Haskell-Cafe@
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
-- View this message in context: http://haskell.1045720.n5.nabble.com/Type-error-depending-on-scope-of-patter... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
And what's Reverse? I happen to know Reifies. But you'll also get a better (and more likely) answer if you reduce dependencies.
Richard
On Aug 1, 2015, at 8:05 PM, htebalaka
Alright. The first two examples show the issue and a fix for it; the last two have the same issue but existential quantification prevents the fix.
grad has type "(Num a, Traversable t) => (forall s. Reifies s Tape => t (Reverse s a) -> Reverse s a) -> t a -> t a", and I'm basically trying to supply a function to it, either by being polymorphic over all Num (of which Reverse s a is an instance), or by providing the specific 'Reifies s Tape => ...' type, neither of which are working.
amindfv wrote
You'll probably get more responses if you paste the code inline.
tom
El Aug 1, 2015, a las 11:25, htebalaka <
goodingm@
> escribió:
I'm curious if anyone can tell me why moving the pattern matching in these two examples makes it fail to compile, and what can be done to resolve the same issue in either of the latter two examples. As far as I can tell these should be equivalent. Unfortunately the solution used in the first examples won't work in the later ones due to the existential quantification. I've been asking on #haskell for a few days but haven't been able to find anyone who knows what the issue is.
Code is available here: http://lpaste.net/137586 <http://lpaste.net/137586>;
-- View this message in context: http://haskell.1045720.n5.nabble.com/Type-error-depending-on-scope-of-patter... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. _______________________________________________ Haskell-Cafe mailing list
Haskell-Cafe@
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Haskell-Cafe mailing list
Haskell-Cafe@
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
-- View this message in context: http://haskell.1045720.n5.nabble.com/Type-error-depending-on-scope-of-patter... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
I managed to remove the Data.Reflection and Numeric.AD dependency entirely. In this case, Reverse is just a newtyped Num with a phantom variable added. Still, the same issue occurs. In one case the type gets defaulted to Integer if I try to pass a "forall a. Num a => t a -> a" to grad (which has type "Num a, Traversable t => (forall s. t (Reverse s a) -> Reverse s a) -> t a -> t a"). Then it complains that Integer isn't Reverse s a, and won't compile. In the other where I try to specifically pass the a value with type "forall s. t (Reverse s a) -> Reverse s a" it think the type variable would escape its scope, but I don't see why it should, or how to prevent that in the "doesnt3" example. I have no idea how to apply the fix used in the first two examples to the later two, or why it should even be necessary. -- View this message in context: http://haskell.1045720.n5.nabble.com/Type-error-depending-on-scope-of-patter... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
I guess that pattern matching on (P f) removes the universal quantification you placed on it and it just defaults to Integer. Seems to be related to https://ghc.haskell.org/trac/ghc/ticket/10450. On 8/3/2015 6:43 PM, htebalaka wrote:
I managed to remove the Data.Reflection and Numeric.AD dependency entirely. In this case, Reverse is just a newtyped Num with a phantom variable added. Still, the same issue occurs. In one case the type gets defaulted to Integer if I try to pass a "forall a. Num a => t a -> a" to grad (which has type "Num a, Traversable t => (forall s. t (Reverse s a) -> Reverse s a) -> t a -> t a"). Then it complains that Integer isn't Reverse s a, and won't compile.
In the other where I try to specifically pass the a value with type "forall s. t (Reverse s a) -> Reverse s a" it think the type variable would escape its scope, but I don't see why it should, or how to prevent that in the "doesnt3" example.
I have no idea how to apply the fix used in the first two examples to the later two, or why it should even be necessary.
-- View this message in context: http://haskell.1045720.n5.nabble.com/Type-error-depending-on-scope-of-patter... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Yeah, that seems to be the issue, but pattern matching with let doesn't seem to work well with existentials, (GHC's brain explodes, and informs me to use a case statement), so the fix there doesn't seem to work either :( David Kraeutmann wrote
I guess that pattern matching on (P f) removes the universal quantification you placed on it and it just defaults to Integer. Seems to be related to https://ghc.haskell.org/trac/ghc/ticket/10450.
On 8/3/2015 6:43 PM, htebalaka wrote:
I managed to remove the Data.Reflection and Numeric.AD dependency entirely. In this case, Reverse is just a newtyped Num with a phantom variable added. Still, the same issue occurs. In one case the type gets defaulted to Integer if I try to pass a "forall a. Num a => t a -> a" to grad (which has type "Num a, Traversable t => (forall s. t (Reverse s a) -> Reverse s a) -> t a -> t a"). Then it complains that Integer isn't Reverse s a, and won't compile.
In the other where I try to specifically pass the a value with type "forall s. t (Reverse s a) -> Reverse s a" it think the type variable would escape its scope, but I don't see why it should, or how to prevent that in the "doesnt3" example.
I have no idea how to apply the fix used in the first two examples to the later two, or why it should even be necessary.
-- View this message in context: http://haskell.1045720.n5.nabble.com/Type-error-depending-on-scope-of-patter... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. _______________________________________________ Haskell-Cafe mailing list
Haskell-Cafe@
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list
Haskell-Cafe@
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
smime.p7s (5K) <http://haskell.1045720.n5.nabble.com/attachment/5814903/0/smime.p7s>;
-- View this message in context: http://haskell.1045720.n5.nabble.com/Type-error-depending-on-scope-of-patter... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
Yeah, that seems to be the issue, but pattern matching with let doesn't seem to work well with existentials, (GHC's brain explodes, and informs me to use a case statement), so the fix there doesn't seem to work either :( David Kraeutmann wrote
I guess that pattern matching on (P f) removes the universal quantification you placed on it and it just defaults to Integer. Seems to be related to https://ghc.haskell.org/trac/ghc/ticket/10450.
On 8/3/2015 6:43 PM, htebalaka wrote:
I managed to remove the Data.Reflection and Numeric.AD dependency entirely. In this case, Reverse is just a newtyped Num with a phantom variable added. Still, the same issue occurs. In one case the type gets defaulted to Integer if I try to pass a "forall a. Num a => t a -> a" to grad (which has type "Num a, Traversable t => (forall s. t (Reverse s a) -> Reverse s a) -> t a -> t a"). Then it complains that Integer isn't Reverse s a, and won't compile.
In the other where I try to specifically pass the a value with type "forall s. t (Reverse s a) -> Reverse s a" it think the type variable would escape its scope, but I don't see why it should, or how to prevent that in the "doesnt3" example.
I have no idea how to apply the fix used in the first two examples to the later two, or why it should even be necessary.
-- View this message in context: http://haskell.1045720.n5.nabble.com/Type-error-depending-on-scope-of-patter... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. _______________________________________________ Haskell-Cafe mailing list
Haskell-Cafe@
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list
Haskell-Cafe@
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
smime.p7s (5K) <http://haskell.1045720.n5.nabble.com/attachment/5814903/0/smime.p7s>;
-- View this message in context: http://haskell.1045720.n5.nabble.com/Type-error-depending-on-scope-of-patter... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
participants (4)
-
amindfv＠gmail.com -
David Kraeutmann -
htebalaka -
Richard Eisenberg