Strange problem with inference
Hi Cafe, I've been playing around with lens and stumbled upon strange GHC behaviour. Consider this source (using lens package and GHC 7.10.2): {-# LANGUAGE TypeFamilies #-} import Control.Lens class Test a where type TestT a myiso :: Iso' a (TestT a) test1 :: Test a => a -> TestT a test1 = view myiso test2 :: Test a => TestT a -> a test2 = view (from myiso) GHC would emit this error: /tmp/test.hs:13:9: Could not deduce (Control.Monad.Reader.Class.MonadReader (TestT a) ((->) (TestT a))) arising from a use of ‘view’ from the context (Test a) bound by the type signature for test2 :: Test a => TestT a -> a at /tmp/test.hs:12:10-31 In the expression: view (from myiso) In an equation for ‘test2’: test2 = view (from myiso) Failed, modules loaded: none. However, `MonadReader r ((->) r)` is defined for any and all `r`! Furthermore, `test1` has no problem with this and `view` there uses this instance too. The only difference that I see is the presence of a type family: * `test1` needs `MonadReader a ((->) a)` * `test2` needs `MonadReader (TestT a) ((->) (TestT a))` , but I don't understand how can this result in a different behavior. Notice that this likely may be reproduced somehow without lens -- I've spent some time trying to minify this example further but alas to no avail. Thanks in advance! -- Nikolay.
One possible fix (tested on GHC-7.10.1 with lens-4.12.3): test2 :: (Test a, t ~ TestT a) => t -> a test2 = view (from myiso) This might have something to do with type families not being injective, but I'm not completely sure. I also agree that it might be possible to trigger this without lens, will try to find an example and post if I succeed. On 11 September 2015 at 05:28, Nikolay Amiantov <ab@fmap.me> wrote:
Hi Cafe,
I've been playing around with lens and stumbled upon strange GHC behaviour. Consider this source (using lens package and GHC 7.10.2):
{-# LANGUAGE TypeFamilies #-}
import Control.Lens
class Test a where type TestT a myiso :: Iso' a (TestT a)
test1 :: Test a => a -> TestT a test1 = view myiso
test2 :: Test a => TestT a -> a test2 = view (from myiso)
GHC would emit this error:
/tmp/test.hs:13:9: Could not deduce (Control.Monad.Reader.Class.MonadReader (TestT a) ((->) (TestT a))) arising from a use of ‘view’ from the context (Test a) bound by the type signature for test2 :: Test a => TestT a -> a at /tmp/test.hs:12:10-31 In the expression: view (from myiso) In an equation for ‘test2’: test2 = view (from myiso) Failed, modules loaded: none.
However, `MonadReader r ((->) r)` is defined for any and all `r`! Furthermore, `test1` has no problem with this and `view` there uses this instance too. The only difference that I see is the presence of a type family:
* `test1` needs `MonadReader a ((->) a)` * `test2` needs `MonadReader (TestT a) ((->) (TestT a))`
, but I don't understand how can this result in a different behavior. Notice that this likely may be reproduced somehow without lens -- I've spent some time trying to minify this example further but alas to no avail.
Thanks in advance!
-- Nikolay. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
-- Regards Sumit Sahrawat
An interesting fix, indeed! I think this might be a bug in GHC -- these should (if I understand correctly) be equivalent signatures. I'll try to find a simpler example too before reporting this, it might shed some light on things (maybe even enough to show this isn't a bug at all ^_^). On 09/11/2015 05:17 AM, Sumit Sahrawat, Maths & Computing, IIT (BHU) wrote:
One possible fix (tested on GHC-7.10.1 with lens-4.12.3):
test2 :: (Test a, t ~ TestT a) => t -> a test2 = view (from myiso)
This might have something to do with type families not being injective, but I'm not completely sure.
I also agree that it might be possible to trigger this without lens, will try to find an example and post if I succeed. -- Nikolay.
~ isn't equivalent. Type signatures are solved by unification and then all occurring constraints are solved. By putting a ~ constraint you explicitly instruct GHC to not attempt unification. When using associated type synonyms you need to use ~, as the choice of TestT a depends on what instance is picked for Test a. There doesn't even have to be an instance at all. As the unifier is iirc mostly independent from the constraint solver, you get that error. See the relevant paper "Associated Type Synonyms" for details.
I've tested with ghc-7.8.4, and the test1/test2 definitions are accepted if you use -XNoMonomorphismRestriction. For test2 to work without annotating a result type, you could use a superclass constraint to show that the type family has an inverse. In ghc-7.10 it doesn't work (see https://ghc.haskell.org/trac/ghc/ticket/10009) https://gist.github.com/aavogt/7a10024f0199dc2e8478 shows both features. On Thu, Sep 10, 2015 at 10:17 PM, Sumit Sahrawat, Maths & Computing, IIT (BHU) <sumit.sahrawat.apm13@iitbhu.ac.in> wrote:
One possible fix (tested on GHC-7.10.1 with lens-4.12.3):
test2 :: (Test a, t ~ TestT a) => t -> a test2 = view (from myiso)
This might have something to do with type families not being injective, but I'm not completely sure.
I also agree that it might be possible to trigger this without lens, will try to find an example and post if I succeed.
On 11 September 2015 at 05:28, Nikolay Amiantov <ab@fmap.me> wrote:
Hi Cafe,
I've been playing around with lens and stumbled upon strange GHC behaviour. Consider this source (using lens package and GHC 7.10.2):
{-# LANGUAGE TypeFamilies #-}
import Control.Lens
class Test a where type TestT a myiso :: Iso' a (TestT a)
test1 :: Test a => a -> TestT a test1 = view myiso
test2 :: Test a => TestT a -> a test2 = view (from myiso)
GHC would emit this error:
/tmp/test.hs:13:9: Could not deduce (Control.Monad.Reader.Class.MonadReader (TestT a) ((->) (TestT a))) arising from a use of ‘view’ from the context (Test a) bound by the type signature for test2 :: Test a => TestT a -> a at /tmp/test.hs:12:10-31 In the expression: view (from myiso) In an equation for ‘test2’: test2 = view (from myiso) Failed, modules loaded: none.
However, `MonadReader r ((->) r)` is defined for any and all `r`! Furthermore, `test1` has no problem with this and `view` there uses this instance too. The only difference that I see is the presence of a type family:
* `test1` needs `MonadReader a ((->) a)` * `test2` needs `MonadReader (TestT a) ((->) (TestT a))`
, but I don't understand how can this result in a different behavior. Notice that this likely may be reproduced somehow without lens -- I've spent some time trying to minify this example further but alas to no avail.
Thanks in advance!
-- Nikolay. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
-- Regards
Sumit Sahrawat
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Thank you all for responses! There are always more things to learn ^_^. I'll also take a look at the paper to understand better what's going on. On 09/11/2015 02:58 AM, Nikolay Amiantov wrote:
Hi Cafe,
I've been playing around with lens and stumbled upon strange GHC behaviour. Consider this source (using lens package and GHC 7.10.2):
{-# LANGUAGE TypeFamilies #-}
import Control.Lens
class Test a where type TestT a myiso :: Iso' a (TestT a)
test1 :: Test a => a -> TestT a test1 = view myiso
test2 :: Test a => TestT a -> a test2 = view (from myiso)
GHC would emit this error:
/tmp/test.hs:13:9: Could not deduce (Control.Monad.Reader.Class.MonadReader (TestT a) ((->) (TestT a))) arising from a use of ‘view’ from the context (Test a) bound by the type signature for test2 :: Test a => TestT a -> a at /tmp/test.hs:12:10-31 In the expression: view (from myiso) In an equation for ‘test2’: test2 = view (from myiso) Failed, modules loaded: none.
However, `MonadReader r ((->) r)` is defined for any and all `r`! Furthermore, `test1` has no problem with this and `view` there uses this instance too. The only difference that I see is the presence of a type family:
* `test1` needs `MonadReader a ((->) a)` * `test2` needs `MonadReader (TestT a) ((->) (TestT a))`
, but I don't understand how can this result in a different behavior. Notice that this likely may be reproduced somehow without lens -- I've spent some time trying to minify this example further but alas to no avail.
Thanks in advance!
-- Nikolay.
participants (4)
-
adam vogt -
David Kraeutmann -
Nikolay Amiantov -
Sumit Sahrawat, Maths & Computing, IIT (BHU)