[GHC] #9210: "overlapping instances" through FunctionalDependencies

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
13 messages Options
Reply | Threaded
Open this post in threaded view
|

[GHC] #9210: "overlapping instances" through FunctionalDependencies

GHC - devs mailing list
#9210: "overlapping instances" through FunctionalDependencies
-------------------------------------------+-------------------------------
       Reporter:  rwbarton                 |             Owner:
           Type:  bug                      |            Status:  new
       Priority:  normal                   |         Milestone:
      Component:  Compiler (Type checker)  |           Version:  7.8.1
       Keywords:                           |  Operating System:
   Architecture:  Unknown/Multiple         |  Unknown/Multiple
     Difficulty:  Unknown                  |   Type of failure:
     Blocked By:                           |  None/Unknown
Related Tickets:                           |         Test Case:
                                           |          Blocking:
-------------------------------------------+-------------------------------
 This program prints `("1",2)`, but if you reverse the order of the two
 instances, it prints `(1,"2")`.

 {{{
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FunctionalDependencies #-}

 -- extracted from http://lpaste.net/105656

 import Control.Applicative
 import Data.Functor.Identity

 modify :: ((a -> Identity b) -> s -> Identity t) -> (a -> b) -> (s -> t)
 modify l f s = runIdentity (l (Identity . f) s)

 class Foo s t a b | a b s -> t where
   foo :: Applicative f => (a -> f b) -> s -> f t

 instance Foo (x, a) (y, a) x y where
   foo f (a,b) = (\fa -> (fa,b)) <$> f a

 instance Foo (a, x) (a, y) x y where
   foo f (a,b) = (\fb -> (a,fb)) <$> f b

 main = print $ modify foo (show :: Int -> String) (1 :: Int, 2 :: Int)
 }}}

 Note that the two instances involved `Foo (Int, Int) (String, Int) Int
 String` and `Foo (Int, Int) (Int, String) Int String` are not actually
 overlapping. But, they have the same `a`, `b`, and `s` fields and it seems
 that this makes GHC think that either one is equally valid, thanks to the
 fundep.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9210>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #9210: "overlapping instances" through FunctionalDependencies

GHC - devs mailing list
#9210: "overlapping instances" through FunctionalDependencies
--------------------------------------------+------------------------------
        Reporter:  rwbarton                 |            Owner:
            Type:  bug                      |           Status:  new
        Priority:  normal                   |        Milestone:
       Component:  Compiler (Type checker)  |          Version:  7.8.1
      Resolution:                           |         Keywords:
Operating System:  Unknown/Multiple         |     Architecture:
 Type of failure:  None/Unknown             |  Unknown/Multiple
       Test Case:                           |       Difficulty:  Unknown
        Blocking:                           |       Blocked By:
                                            |  Related Tickets:
--------------------------------------------+------------------------------
Changes (by ekmett):

 * cc: ekmett@… (added)


--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9210#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #9210: "overlapping instances" through FunctionalDependencies

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#9210: "overlapping instances" through FunctionalDependencies
--------------------------------------------+------------------------------
        Reporter:  rwbarton                 |            Owner:
            Type:  bug                      |           Status:  new
        Priority:  normal                   |        Milestone:
       Component:  Compiler (Type checker)  |          Version:  7.8.2
      Resolution:                           |         Keywords:
Operating System:  Unknown/Multiple         |     Architecture:
 Type of failure:  None/Unknown             |  Unknown/Multiple
       Test Case:                           |       Difficulty:  Unknown
        Blocking:                           |       Blocked By:
                                            |  Related Tickets:
--------------------------------------------+------------------------------
Changes (by rwbarton):

 * version:  7.8.1 => 7.8.2


Comment:

 Oh, since I minimized the example now I can test more easily with other
 GHC versions.

 This is a regression from GHC 7.6.3, in that that version rejected `main`
 with the following error (that I don't really understand):
 {{{
 some.hs:22:23:
     Couldn't match type `Int' with `String'
     When using functional dependencies to combine
       Foo (a, x) (a, y) x y,
         arising from the dependency `a b s -> t'
         in the instance declaration at some.hs:19:10
       Foo (Int, Int) (String, Int) Int String,
         arising from a use of `foo' at some.hs:22:23-25
     In the first argument of `modify', namely `foo'
     In the second argument of `($)', namely
       `modify foo (show :: Int -> String) (1 :: Int, 2 :: Int)'
 Failed, modules loaded: none.
 }}}
 If I remove `main` then GHC 7.6.3 does accept the instances, though. That
 seems wrong to me also (though certainly "less wrong").

 I have a GHC 7.8.2.20140609 lying around and it displays the same behavior
 as GHC 7.8.1.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9210#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #9210: "overlapping instances" through FunctionalDependencies

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#9210: "overlapping instances" through FunctionalDependencies
--------------------------------------------+------------------------------
        Reporter:  rwbarton                 |            Owner:
            Type:  bug                      |           Status:  new
        Priority:  normal                   |        Milestone:
       Component:  Compiler (Type checker)  |          Version:  7.8.2
      Resolution:                           |         Keywords:
Operating System:  Unknown/Multiple         |     Architecture:
 Type of failure:  None/Unknown             |  Unknown/Multiple
       Test Case:                           |       Difficulty:  Unknown
        Blocking:                           |       Blocked By:
                                            |  Related Tickets:
--------------------------------------------+------------------------------
Changes (by simonpj):

 * cc: dimitris@…, diatchki (added)


Comment:

 I can at least explain what is going on. I defer to Iavor (the Functional
 Dependency Expert) on what the right thing to do might be.

 == Problem 1: Should these instance declarations be accepted at all?  ==

 After all, unifying the a,b,s components of the instances shows that the
 constraint `Foo (x,x) ?? x y` would match both instances, and hence (via
 the fundep) force `??` to be both `(y,x)` and `(x,y)` respectively.

 GHC doesn't currently complain about this, I think because there are some
 yet-more-specific constraints that would not give rise to a conflict. For
 example, suppose I was trying to solve `(Foo (Int,Int) ?? Int Int)`. Then
 both fundeps would compatibly force `??` to be `(Int,Int)`.  Mind you,
 then the overlap checker would say that it couldn't pick which of the two
 instances to use.

 So my instinct is that this check for "yet-more-specific" constraints is
 wrong.  If the things on the LHS of the fundep arrow unify, then the
 things on the RHS should be equal. That would reject these two instance
 declarations. Iavor?

 For completeness, the offending bit of code is this, in `FunDeps.lhs` line
 318
 {{{
         Just subst | isJust (tcUnifyTys bind_fn rtys1' rtys2')
                         -- Don't include any equations that already hold.
                         -- Reason: then we know if any actual improvement
 has happened,
                         --         in which case we need to iterate the
 solver
                         -- In making this check we must taking account of
 the fact that any
                         -- qtvs that aren't already instantiated can be
 instantiated to anything
                         -- at all
 }}}

 == Problem 2: why does type checking succeed? ==

 The second mystery is this: why is the constraint `(Foo (Int,Int) alpha
 Int String)`, which is what arises from `main`, solved without error?
 `alpha` is a unification variable. What happens is this.
  * The constraint gives rise to two derived constraints, one from each
 fundep `[D] alpha ~ (Int,String)` and `[D] alpha ~ (String,Int)`.
  * The first is solved by `alpha := (Int,String)`.
  * Having made that choice, the constraint `Foo (Int,Int) (Int,String) Int
 String` uniquely matches the second instance declaration, and so can be
 solved.
  * The second derived constraint becomes `[D] (Int,String) ~ (String,Int)`
 and therefore leads to two isoluble derived constraints `[D] Int ~ String`
 and `[D] String ~ Int`.
  * But if we manage to solve everything else, we discard insoluble derived
 constraints; see `Note [Dropping derived constraints]` in `TcRnTypes`.

 As a result of all this, we (totally bogusly) pick one instance
 declaration, ignoring the fact that the other matches too. Ugh!

 I'm not quite sure what to do, but let's sort out (1) before thinking
 about (2).  Iavor?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9210#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #9210: "overlapping instances" through FunctionalDependencies

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#9210: "overlapping instances" through FunctionalDependencies
--------------------------------------------+------------------------------
        Reporter:  rwbarton                 |            Owner:
            Type:  bug                      |           Status:  new
        Priority:  normal                   |        Milestone:
       Component:  Compiler (Type checker)  |          Version:  7.8.2
      Resolution:                           |         Keywords:
Operating System:  Unknown/Multiple         |     Architecture:
 Type of failure:  None/Unknown             |  Unknown/Multiple
       Test Case:                           |       Difficulty:  Unknown
        Blocking:                           |       Blocked By:
                                            |  Related Tickets:
--------------------------------------------+------------------------------
Changes (by simonpj):

 * cc: dreixel (added)


Comment:

 OK, well I tried the effect of solving problem 1 by making the two
 instance declarations illegal.  The changes in FunDeps are simple:
  * Remove altogether the alternative guarded by `| isJust (tcUnifyTys
 bind_fn rtys1' rtys2')`, mentioned above
  * Change the definition of `fdeqs` thus
 {{{
 -                    fdeqs = zipAndComputeFDEqs (\_ _ -> False) rtys1'
 irs2'
 +                    fdeqs = zipAndComputeFDEqs eqType rtys1' irs2'
 }}}
 This resulted in four test-suite failures
 {{{
 Unexpected failures:
    ghci/scripts              ghci047 [bad stderr] (ghci)
    polykinds                 T9106 [stderr mismatch] (normal)
    typecheck/should_compile  FD4 [exit code non-0] (normal)
    typecheck/should_compile  T7875 [exit code non-0] (normal)
 }}}
 All were for the same reason: instance declarations that were previously
 accepted are now rejected.

 I looked a bit more at `T7875`.  It is described by `Note [Weird fundeps]`
 in `TcInteract`, which reads as follows:
 {{{
 Note [Weird fundeps]
 ~~~~~~~~~~~~~~~~~~~~
 Consider   class Het a b | a -> b where
               het :: m (f c) -> a -> m b

            class GHet (a :: * -> *) (b :: * -> *) | a -> b
            instance            GHet (K a) (K [a])
            instance Het a b => GHet (K a) (K b)

 The two instances don't actually conflict on their fundeps,
 although it's pretty strange.  So they are both accepted. Now
 try   [W] GHet (K Int) (K Bool)
 This triggers fudeps from both instance decls; but it also
 matches a *unique* instance decl, and we should go ahead and
 pick that one right now.  Otherwise, if we don't, it ends up
 unsolved in the inert set and is reported as an error.

 Trac #7875 is a case in point.
 }}}
 This does indeed look weird to me. And it's incredibly fragile.  If the
 wanted constraint doesn't '''yet''' match a unique instance decl (perhaps
 because some other constraint has not yet done a unification) then we
 won't pick the instance, so we will generate both (conflicting) fundeps,
 and we will get an error (from the fundep) even though the constraint is
 ultimately solved.  This seems terrible to me.   So I think I'd argue that
 #7875 should be rejected (hence adding Pedro, its author, in cc).

 `FD4` actually comes from #1797, and involves a combination of functional
 dependencies and overlapping instances.  I'm not sure we've ever fully
 thought through this conbination, but rejecting this would indeed make
 people unhappy.

 I have not looked at #9106 or `ghci047`.

 I feel strongly disinclined to dive once more into the functional
 dependency swamp.  If someone (Iavor?  Pedro?) would like to help that
 would be great.

 Until then, I totally agree that the behaviour of this ticket is bizarre
 and wrong. But without help I don't know how to fix it.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9210#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #9210: "overlapping instances" through FunctionalDependencies

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#9210: "overlapping instances" through FunctionalDependencies
-------------------------------------+-------------------------------------
        Reporter:  rwbarton          |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.8.2
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by rwbarton):

 Somehow, this program no longer compiles in GHC 8.0 or HEAD. Yay!

 I'd rather not just close this without knowing why it was fixed, and we
 should add a regression test.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9210#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #9210: "overlapping instances" through FunctionalDependencies

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#9210: "overlapping instances" through FunctionalDependencies
-------------------------------------+-------------------------------------
        Reporter:  rwbarton          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.8.2
  checker)                           |
      Resolution:                    |             Keywords:  FunDeps
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by AntC):

 * keywords:   => FunDeps


--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9210#comment:6>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #9210: "overlapping instances" through FunctionalDependencies

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#9210: "overlapping instances" through FunctionalDependencies
-------------------------------------+-------------------------------------
        Reporter:  rwbarton          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.8.2
  checker)                           |
      Resolution:                    |             Keywords:  FunDeps
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by diatchki):

 Here is a simplified version of the example in the ticket:
 {{{
 class Foo a b c | a b -> c

 instance Foo (x, a) x ((), a)
 instance Foo (x, a) a (x, ())
 }}}

 These two instances are accepted by GHC 8.0.1, but should be rejected as
 they violate the FD on the class. Here is the counter example:
 {{{
 Foo (Int,Int) Int ((), Int)
 Foo (Int,Int) Int (Int, ())
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9210#comment:7>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #9210: "overlapping instances" through FunctionalDependencies

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#9210: "overlapping instances" through FunctionalDependencies
-------------------------------------+-------------------------------------
        Reporter:  rwbarton          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.8.2
  checker)                           |
      Resolution:                    |             Keywords:  FunDeps
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by AntC):

 Replying to [comment:7 diatchki]:
 > Here is a simplified version of the example in the ticket:

 Thanks Iavor, are you sure this is the ticket you meant? This one is about
 the order of declaration of instances affecting type inference, and the
 problem seems to have cleared up, according to comment:5.

 > {{{
 > class Foo a b c | a b -> c
 >
 > instance Foo (x, a) x ((), a)
 > instance Foo (x, a) a (x, ())
 > }}}
 >
 > These two instances are accepted by GHC 8.0.1, ...

 You mean the instance decls compile? They partially overlap, so GHC will
 delay any error reporting until a use site.

 > ... but should be rejected as they violate the FD on the class.

 They're inconsistent only for the cases of overlap per your counter-
 example below, not in general. That is, not when `x` is different to `a`.

 > Here is the counter example:
 > {{{
 > Foo (Int,Int) Int ((), Int)
 > Foo (Int,Int) Int (Int, ())
 > }}}
 >

 I get attempts at those usages roundly rejected by GHC. (It suggested I
 `AllowAmbiguousTypes`, but that didn't help. I also switched on
 `UndecidableInstances` to give it maximum help.)

 {{{
 {-# LANGUAGE   MultiParamTypeClasses, FunctionalDependencies,
               FlexibleInstances, FlexibleContexts,
               AllowAmbiguousTypes, UndecidableInstances   #-}

 class Foo a b c | a b -> c where { foo :: a -> b -> c }

 instance Foo (x, a) x ((), a) where foo (x, a) x2 = ((), a)
 instance Foo (x, a) a (x, ()) where foo (x, a) a2 = (x, ())

 f1 = foo (True, 'c') False
 f2 = foo (True, 'd') 'e'
 f3 = foo (5 :: Int, 7 :: Int) (9 :: Int)

 main = print $ "results" ++ show f1 ++ show f2  ++ show f3

 prog.hs:12:6: error:
     • Couldn't match type ‘Int’ with ‘()’
         arising from a functional dependency between:
           constraint ‘Foo (Int, Int) Int (Int, ())’
             arising from a use of ‘foo’
           instance ‘Foo (x, a) x ((), a)’ at prog.hs:7:10-29
     • In the expression: foo (5 :: Int, 7 :: Int) (9 :: Int)
       In an equation for ‘f3’: f3 = foo (5 :: Int, 7 :: Int) (9 :: Int)

 }}}

 (Per the O.P., if I switch round the order of those instance declarations,
 I do get a different error message, essentially just a mirror image.)

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9210#comment:8>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #9210: "overlapping instances" through FunctionalDependencies

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#9210: "overlapping instances" through FunctionalDependencies
-------------------------------------+-------------------------------------
        Reporter:  rwbarton          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.8.2
  checker)                           |
      Resolution:                    |             Keywords:  FunDeps
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by diatchki):

 I mean that the example I gave should be rejected, but the program is
 accepted.

 The check for FD consistency is done when multiple instances come
 together, not when you use them.  This is necessary, because it ensures
 that the FD invariant on the class holds, and then we can use the
 invariant in whatever context we want.  For the same reason, you can't
 have instances be consistent only in some cases.

 Currently GHC is very conservative in its use of FDs---it uses them only
 for type inference.  This is why having inconsistent instances like the
 example I showed is not the end of the world: it may result in odd
 behavior where GHC sometimes infers the one type and sometimes the other,
 but the final result is still a sound Haskell program.

 For example, if GHC encountered a constraint `Foo (Int,Int) Int a`, where
 `a` is a unification variable, it might instantiate `a` as either
 `((),Int)` or `(Int,())` depending on in what order it happened to consult
 the instances.  This is essentially the problem that was reported in the
 ticket.

 However, if GHC was to start using the FDs fully as they were intended,
 having inconsistent instances would lead to unsound type-checking. For
 example, in this case, GHC should be able to prove that `((),Int) ~
 (Int,())`, which is obviously bogus.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9210#comment:9>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #9210: "overlapping instances" through FunctionalDependencies

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#9210: "overlapping instances" through FunctionalDependencies
-------------------------------------+-------------------------------------
        Reporter:  rwbarton          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.8.2
  checker)                           |
      Resolution:                    |             Keywords:  FunDeps
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by AntC):

 Replying to [comment:9 diatchki]:
 > I mean that the example I gave should be rejected, but the program is
 accepted.
 >

 Sorry, Iavor, I'm not following. GHC as at 8.0.1 seems to be behaving as
 documented here
 http://downloads.haskell.org/~ghc/8.0.2/docs/html/users_guide/glasgow_exts.html
 #instance-resolution

  * It is fine for there to be a ''potential'' of overlap (...); an error
 is only reported if a particular constraint matches more than one
 [instance].
 .

 >
 > The check for FD consistency is done when multiple instances come
 together, not when you use them.

 Are you saying this is what you'd like to see happening? What GHC is
 actually doing is checking FD consistency when it sees the instance decls,
 and only rejecting if the instances are outright contradictory. If there's
 only a ''potential'' inconsistency (due to overlap), GHC only rejects at
 the use site if it can't resolve to a particular instance.

 .
 >
 > This is necessary, because it ensures that the FD invariant on the class
 holds, and then we can use the invariant in whatever context we want.  For
 the same reason, you can't have instances be consistent only in some
 cases.
 >

 Again, I think you're saying you'd like to be able to "use the
 invariant"/rely on them being consistent(?)

 .
 >
 > Currently GHC is very conservative in its use of FDs---it uses them only
 for type inference.

 Yes GHC is conservative. Whereas in the FDs-via-CHRs paper, it is expected
 that under an FD `C a b | a -> b` if we have `C a b` and `C a b'` we can
 conclude `b = b'` (that's type equality, not just unifiability); GHC does
 not arrive at any such conclusion.

 .
 >
 > This is why having inconsistent instances like the example I showed is
 not the end of the world: it may result in odd behavior where GHC
 sometimes infers the one type and sometimes the other, but the final
 result is still a sound Haskell program.
 >
 > For example, if GHC encountered a constraint `Foo (Int,Int) Int a`,
 where `a` is a unification variable, it might instantiate `a` as either
 `((),Int)` or `(Int,())` depending on in what order it happened to consult
 the instances.  This is essentially the problem that was reported in the
 ticket.
 >

 Yes that is the problem reported on the ticket. AFAICT is was still a
 problem at 7.10. I see no evidence it is still happening at 8.0. (I've
 tried the same code at both versions.) I agree with @Reid it's rather
 discomforting this change of behaviour can't be nailed down to a specific
 mod.

 What you can still do in 8.0 is put a type signature, to get inconsistent
 behaviour:

 {{{
 f4 = foo (5 :: Int, 7 :: Int) (9 :: Int) :: ((), Int)     -- results in
 ((), 7)
 f5 = foo (5 :: Int, 7 :: Int) (9 :: Int) :: (Int, ())     -- results in
 (5, ())
 }}}

 .
 > However, if GHC was to start using the FDs fully as they were intended,
 having inconsistent instances would lead to unsound type-checking. For
 example, in this case, GHC should be able to prove that `((),Int) ~
 (Int,())`, which is obviously bogus.

 Hmm. "as they were intended" is rather debatable. For each of the examples
 you're bringing forward, you're using several extensions of Haskell beyond
 Haskell 2010: `UndecidableInstances` or non-full dependencies (in a way
 that breaks the FDs-via-CHRs rules) or overlap -- either
 `OverlappingInstances` or overlap of the types in a non-full dependency.
 In this case we're now discussing you need `FlexibleInstances`, again not
 envisaged in the paper.

 I think each of those extensions is justifiable. Furthermore for GHC to be
 using FD inference as per the FDs-via-CHRs rules would block separate
 compilation. (The CHRs assume you can see all instance decls.) So I think
 it's prudent GHC does not try to go that far, and therefore avoids the
 risk of unsound type-checking.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9210#comment:10>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #9210: "overlapping instances" through FunctionalDependencies

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#9210: "overlapping instances" through FunctionalDependencies
-------------------------------------+-------------------------------------
        Reporter:  rwbarton          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.8.2
  checker)                           |
      Resolution:                    |             Keywords:  FunDeps
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by diatchki):

 The check for overlapping is done when GHC resolves instances. This is
 unrelated to this example. You can easily modify it, so that there are no
 overlapping instances:

 {{{
 class Foo tag a b c | a b -> c

 instance Foo Int (x, a) x ((), a)
 instance Foo Bool (x, a) a (x, ())
 }}}

 The check for the consistency of FDs ought to be done whenever instances
 exist in the same scope, and there are two ways in which this can happen:

    1. they were declared in the same module, in which case GHC will try to
 check their consistency---as this example illustrates, we have a bug in
 the checking code, as the instances are not reported as inconsistent;

    2. when instances are imported into the same module.  In this case GHC
 doesn't try to validate the comparability of the instances at all, which
 leads to obviously inconsistent FDs (e.g., `F Int Int` in one module, `F
 Int Char` in another, and both are  OK when imported in a third module).
 It also leads to the fairly well-known bug of incoherent instances where
 GHC will happily allow two different instances for the same type tp be
 used in different modules.


 As far as I can tell, the new behavior in 8 is how GHC uses FDs to perform
 improvements.  Instead of just using one of the instances, it will now try
 to improve with all of the instances.  As a result, if there are
 inconsistencies, it will try to improve in two different ways, and report
 a delayed error.

 The underlying bug of failing to detect the inconsistency of the instances
 is still present.

 The thing that we should be checking is:
 {{{
 forall x1 a2 x2 a2. ( (x1,a1) ~ (x2,a2), x1 ~ a2 ) => ( ((), a1) ~ (x2,
 ()) )
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9210#comment:11>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #9210: "overlapping instances" through FunctionalDependencies

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#9210: "overlapping instances" through FunctionalDependencies
-------------------------------------+-------------------------------------
        Reporter:  rwbarton          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.8.2
  checker)                           |
      Resolution:                    |             Keywords:  FunDeps
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by AntC):

 Replying to [comment:11 diatchki]:
 > The check for overlapping is done when GHC resolves instances. This is
 unrelated to this example. You can easily modify it, so that there are no
 overlapping instances:
 >
 > {{{
 > class Foo tag a b c | a b -> c
 >
 > instance Foo Int (x, a) x ((), a)
 > instance Foo Bool (x, a) a (x, ())
 > }}}

 No, that class decl is not allowed, according to the FDs-via-CHRs paper,
 Section 6.2 on Non-full dependencies. (And this example is similar to
 yours on #10675 -- which I think is also disallowed.) If the FD is non-
 full, the class must have a super-class constraint to enforce the FD.
 Otherwise we still get inconsistent behaviour, which is your complaint on
 #10675.

 .
 >
 > The check for the consistency of FDs ought to be done whenever instances
 exist in the same scope, ...

 You mean like dear old Hugs? Yes I miss it for that reason. But I think
 you can still get inconsistent behaviour with overlapping instances, if
 some instances are in scope in one module but different instances in scope
 in a different module.

 I think what it needs is to ban overlap altogether. (And that means for
 non-full FDs, banning overlap of the params involved with that FD. We have
 to be canny there: allow identical params, modulo alpha renaming.) Then we
 just reject any instance that attempts to overlap. (Again Hugs in effect
 did that with its check "Instance is inconsistent with FunDeps".)

 But what we can do currently with overlapping instances is useful. We need
 a more expressive way to say in the instance: yes I know this looks like
 it overlaps, but actually I don't want it to; when the use site appears to
 be ambiguous, always pick that instance. For example with instance guards:

 {{{
 class Foo a b c | a b -> c

 instance Foo (x, a) x ((), a)   | x /~ a
 instance Foo (x, a) a (x, ())
 }}}

 The guard on that first instance says: `x` must not be unifiable with `a`,
 so do not select this instance if unifiable. That's the same as Richard's
 apartness check for Closed Type Families selecting equations. More
 discussion here https://typesandkinds.wordpress.com/2013/04/29/coincident-
 overlap-in-type-families/

 .
 >
 > As far as I can tell, the new behavior in 8 is how GHC uses FDs to
 perform improvements.  Instead of just using one of the instances, it will
 now try to improve with all of the instances.  As a result, if there are
 inconsistencies, it will try to improve in two different ways, and report
 a delayed error.

 "New"? You're describing the behaviour Simon raises in #10675, which was
 at 7.10. And judging by "Examples in the testsuite that exploit this
 loophole ", it's been around for some time. I agree with you that GHC
 should not try to merge or mingle/mangle type improvements from different
 instances. The behaviour in #10675 is just nuts. (But trying to cure it
 might be worse than the disease. It does seem to be a swamp.)

 .
 >
 > The underlying bug of failing to detect the inconsistency of the
 instances is still present.
 >
 > The thing that we should be checking is:
 > {{{
 > forall x1 a2 x2 a2. ( (x1,a1) ~ (x2,a2), x1 ~ a2 ) => ( ((), a1) ~ (x2,
 ()) )
 > }}}

 Yes, which we can do with a superclass constraint, such as a type function
 with equality constraint.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9210#comment:12>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets