[GHC] #13981: Family instance consistency checks happens too early when hs-boot defined type occurs on LHS

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
9 messages Options
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

[GHC] #13981: Family instance consistency checks happens too early when hs-boot defined type occurs on LHS

GHC - devs mailing list
#13981: Family instance consistency checks happens too early when hs-boot defined
type occurs on LHS
-------------------------------------+-------------------------------------
           Reporter:  ezyang         |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1-rc2
  (Type checker)                     |
           Keywords:  hs-boot        |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This is a follow up ticket for #13803, since I wanted to fix the immediate
 bug in #13803 without having to deal with the more complicated case here:

 {{{
 -- F.hs
 {-# LANGUAGE TypeFamilies #-}
 module F where
 type family F a :: *

 -- A.hs-boot
 module A where
 data T

 -- B.hs
 {-# LANGUAGE TypeFamilies #-}
 module B where
 import {-# SOURCE #-} A
 import F
 type instance F T = Int

 -- C.hs
 {-# LANGUAGE TypeFamilies #-}
 module C where
 import {-# SOURCE #-} A
 import F
 type instance F T = Bool

 -- A.hs
 module A where
 import B
 import C
 }}}

 From what I wrote: right now, we decide to defer a type family consistency
 check if the family was recursively defined. If the RHS refers to a
 recursively defined type, there's no problem: we don't need to look at it
 for consistency checking. But if the LHS is recursively defined, as is in
 this example, we DO need to defer the check.

 But it's a bit irritating to figure out whether or not there's actually a
 reference to a recursively defined type in the LHS, since this involves
 traversing the LHS types, and if we're not careful we'll end up pulling in
 the TyThing anyway. There are two other possibilities: (1) always defer
 checking instances which are defined inside the recursive look (by looking
 at the Name of the axiom), or (2) annotating IfaceAxiom with the set of
 boot types its LHS refers to, for easy checking. Not entirely sure what
 the best action is.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13981>
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
|  
Report Content as Inappropriate

Re: [GHC] #13981: Family instance consistency checks happens too early when hs-boot defined type occurs on LHS

GHC - devs mailing list
#13981: Family instance consistency checks happens too early when hs-boot defined
type occurs on LHS
-------------------------------------+-------------------------------------
        Reporter:  ezyang            |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.1-rc2
  checker)                           |
      Resolution:                    |             Keywords:  hs-boot
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 simonpj):

 >  right now, we decide to defer a type family consistency check if the
 family was recursively defined.

 I don't like the sound of that.  Strange deferring under special
 circumstances.  Can we figure out a more uniform approach?

 I've lost context here.  In your example, modules `B` and `C` seem to have
 no overlap problem, but `A` does.   Can you set out the problem you are
 trying to solve, ab-initio?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13981#comment:1>
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
|  
Report Content as Inappropriate

Re: [GHC] #13981: Family instance consistency checks happens too early when hs-boot defined type occurs on LHS

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#13981: Family instance consistency checks happens too early when hs-boot defined
type occurs on LHS
-------------------------------------+-------------------------------------
        Reporter:  ezyang            |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.1-rc2
  checker)                           |
      Resolution:                    |             Keywords:  hs-boot
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 ezyang):

 Yeah. The details are in `Note [Don't check hs-boot type family instances
 too early]`, but reproduced below:

 * So, the origin of a panic "tcIfaceGlobal (local): not found" is when
 force the TyThing of a locally defined type prior to having actually
 typechecked that type. Ordinarily this can't happen (since you can't even
 get your hands on the TyThing before you've typechecked the type), but
 when you have an hs-boot file, a placeholder thunk for the TyThing is put
 into the context, and the onus is on you to avoid forcing this thunk until
 it is ready.

 * Type family consistency checking happens prior to any typechecking, and
 (as first discovered in #11062) it can cause a TyThing of an hs-boot
 defined type family to be forced too early. Originally, I suggested that
 we simply do the consistency check after all typechecking was done. But
 this has its own problem: if we do the consistency check too late, we may
 end up typechecking Haskell code under inconsistent/overlapping sets of
 axioms, which could lead to very strange errors.

 * Thus, we have to defer some of the consistency checks. We first do all
 of the consistency checks that could not possibly force a TyThing
 immediately, and then as we finish kind-checking a type family, we then go
 ahead and do all of the deferred consistency checks involving that family.

 * What I didn't realize when I originally wrote this patch is that the
 early forcing isn't limited just to a type family: types which occur in
 the LHS of overlapping instances (`T` above) also have this problem. So
 some new solution needs to be found.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13981#comment:2>
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
|  
Report Content as Inappropriate

Re: [GHC] #13981: Family instance consistency checks happens too early when hs-boot defined type occurs on LHS

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#13981: Family instance consistency checks happens too early when hs-boot defined
type occurs on LHS
-------------------------------------+-------------------------------------
        Reporter:  ezyang            |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.1-rc2
  checker)                           |
      Resolution:                    |             Keywords:  hs-boot
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by simonpj:

Old description:

> This is a follow up ticket for #13803, since I wanted to fix the
> immediate bug in #13803 without having to deal with the more complicated
> case here:
>
> {{{
> -- F.hs
> {-# LANGUAGE TypeFamilies #-}
> module F where
> type family F a :: *
>
> -- A.hs-boot
> module A where
> data T
>
> -- B.hs
> {-# LANGUAGE TypeFamilies #-}
> module B where
> import {-# SOURCE #-} A
> import F
> type instance F T = Int
>
> -- C.hs
> {-# LANGUAGE TypeFamilies #-}
> module C where
> import {-# SOURCE #-} A
> import F
> type instance F T = Bool
>
> -- A.hs
> module A where
> import B
> import C
> }}}
>
> From what I wrote: right now, we decide to defer a type family
> consistency check if the family was recursively defined. If the RHS
> refers to a recursively defined type, there's no problem: we don't need
> to look at it for consistency checking. But if the LHS is recursively
> defined, as is in this example, we DO need to defer the check.
>
> But it's a bit irritating to figure out whether or not there's actually a
> reference to a recursively defined type in the LHS, since this involves
> traversing the LHS types, and if we're not careful we'll end up pulling
> in the TyThing anyway. There are two other possibilities: (1) always
> defer checking instances which are defined inside the recursive look (by
> looking at the Name of the axiom), or (2) annotating IfaceAxiom with the
> set of boot types its LHS refers to, for easy checking. Not entirely sure
> what the best action is.
New description:

 This is a follow up ticket for #13803, since I wanted to fix the immediate
 bug in #13803 without having to deal with the more complicated case here:

 {{{
 -- F.hs
 {-# LANGUAGE TypeFamilies #-}
 module F where
 type family F a :: *

 -- A.hs-boot
 module A where
 data T

 -- B.hs
 {-# LANGUAGE TypeFamilies #-}
 module B where
 import {-# SOURCE #-} A
 import F
 type instance F T = Int

 -- C.hs
 {-# LANGUAGE TypeFamilies #-}
 module C where
 import {-# SOURCE #-} A
 import F
 type instance F T = Bool

 -- A.hs
 module A where
 import B
 import C

 data T = T
 }}}

 From what I wrote: right now, we decide to defer a type family consistency
 check if the family was recursively defined. If the RHS refers to a
 recursively defined type, there's no problem: we don't need to look at it
 for consistency checking. But if the LHS is recursively defined, as is in
 this example, we DO need to defer the check.

 But it's a bit irritating to figure out whether or not there's actually a
 reference to a recursively defined type in the LHS, since this involves
 traversing the LHS types, and if we're not careful we'll end up pulling in
 the TyThing anyway. There are two other possibilities: (1) always defer
 checking instances which are defined inside the recursive look (by looking
 at the Name of the axiom), or (2) annotating IfaceAxiom with the set of
 boot types its LHS refers to, for easy checking. Not entirely sure what
 the best action is.

--

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13981#comment:3>
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
|  
Report Content as Inappropriate

Re: [GHC] #13981: Family instance consistency checks happens too early when hs-boot defined type occurs on LHS

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#13981: Family instance consistency checks happens too early when hs-boot defined
type occurs on LHS
-------------------------------------+-------------------------------------
        Reporter:  ezyang            |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.1-rc2
  checker)                           |
      Resolution:                    |             Keywords:  hs-boot
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 Ben Gamari <ben@…>):

 In [changeset:"fdb6a5bfd545094782fb539951b561ac2467443d/ghc" fdb6a5b/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="fdb6a5bfd545094782fb539951b561ac2467443d"
 Make IfaceAxiom typechecking lazier.

 Fixes #13803, but adds a note about a yet to be fixed #13981.

 Signed-off-by: Edward Z. Yang <[hidden email]>

 Test Plan: validate

 Reviewers: bgamari, austin

 Reviewed By: bgamari

 Subscribers: simonpj, rwbarton, thomie

 GHC Trac Issues: #13803

 Differential Revision: https://phabricator.haskell.org/D3742
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13981#comment:4>
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
|  
Report Content as Inappropriate

Re: [GHC] #13981: Family instance consistency checks happens too early when hs-boot defined type occurs on LHS

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#13981: Family instance consistency checks happens too early when hs-boot defined
type occurs on LHS
-------------------------------------+-------------------------------------
        Reporter:  ezyang            |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:  8.2.1
       Component:  Compiler (Type    |              Version:  8.2.1-rc2
  checker)                           |
      Resolution:  fixed             |             Keywords:  hs-boot
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 bgamari):

 * status:  new => closed
 * resolution:   => fixed
 * milestone:   => 8.2.1


Old description:

> This is a follow up ticket for #13803, since I wanted to fix the
> immediate bug in #13803 without having to deal with the more complicated
> case here:
>
> {{{
> -- F.hs
> {-# LANGUAGE TypeFamilies #-}
> module F where
> type family F a :: *
>
> -- A.hs-boot
> module A where
> data T
>
> -- B.hs
> {-# LANGUAGE TypeFamilies #-}
> module B where
> import {-# SOURCE #-} A
> import F
> type instance F T = Int
>
> -- C.hs
> {-# LANGUAGE TypeFamilies #-}
> module C where
> import {-# SOURCE #-} A
> import F
> type instance F T = Bool
>
> -- A.hs
> module A where
> import B
> import C
>
> data T = T
> }}}
>
> From what I wrote: right now, we decide to defer a type family
> consistency check if the family was recursively defined. If the RHS
> refers to a recursively defined type, there's no problem: we don't need
> to look at it for consistency checking. But if the LHS is recursively
> defined, as is in this example, we DO need to defer the check.
>
> But it's a bit irritating to figure out whether or not there's actually a
> reference to a recursively defined type in the LHS, since this involves
> traversing the LHS types, and if we're not careful we'll end up pulling
> in the TyThing anyway. There are two other possibilities: (1) always
> defer checking instances which are defined inside the recursive look (by
> looking at the Name of the axiom), or (2) annotating IfaceAxiom with the
> set of boot types its LHS refers to, for easy checking. Not entirely sure
> what the best action is.
New description:

 This is a follow up ticket for #13803, since I wanted to fix the immediate
 bug in #13803 without having to deal with the more complicated case here:

 {{{#!hs
 -- F.hs
 {-# LANGUAGE TypeFamilies #-}
 module F where
 type family F a :: *

 -- A.hs-boot
 module A where
 data T

 -- B.hs
 {-# LANGUAGE TypeFamilies #-}
 module B where
 import {-# SOURCE #-} A
 import F
 type instance F T = Int

 -- C.hs
 {-# LANGUAGE TypeFamilies #-}
 module C where
 import {-# SOURCE #-} A
 import F
 type instance F T = Bool

 -- A.hs
 module A where
 import B
 import C

 data T = T
 }}}

 From what I wrote: right now, we decide to defer a type family consistency
 check if the family was recursively defined. If the RHS refers to a
 recursively defined type, there's no problem: we don't need to look at it
 for consistency checking. But if the LHS is recursively defined, as is in
 this example, we DO need to defer the check.

 But it's a bit irritating to figure out whether or not there's actually a
 reference to a recursively defined type in the LHS, since this involves
 traversing the LHS types, and if we're not careful we'll end up pulling in
 the TyThing anyway. There are two other possibilities: (1) always defer
 checking instances which are defined inside the recursive look (by looking
 at the Name of the axiom), or (2) annotating IfaceAxiom with the set of
 boot types its LHS refers to, for easy checking. Not entirely sure what
 the best action is.

--

Comment:

 Merged to `ghc-8.2` with 31c5c7c5ba8587d6e06782c260db1b3313a05df6.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13981#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
|  
Report Content as Inappropriate

Re: [GHC] #13981: Family instance consistency checks happens too early when hs-boot defined type occurs on LHS

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#13981: Family instance consistency checks happens too early when hs-boot defined
type occurs on LHS
-------------------------------------+-------------------------------------
        Reporter:  ezyang            |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:  8.2.1
       Component:  Compiler (Type    |              Version:  8.2.1-rc2
  checker)                           |
      Resolution:  fixed             |             Keywords:  hs-boot
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 inaki):

 * cc: inaki (added)


--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13981#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
|  
Report Content as Inappropriate

Re: [GHC] #13981: Family instance consistency checks happens too early when hs-boot defined type occurs on LHS

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#13981: Family instance consistency checks happens too early when hs-boot defined
type occurs on LHS
-------------------------------------+-------------------------------------
        Reporter:  ezyang            |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:  8.2.1
       Component:  Compiler (Type    |              Version:  8.2.1-rc2
  checker)                           |
      Resolution:  fixed             |             Keywords:  hs-boot
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 inaki):

 I think that this issue got perhaps closed by mistake?

 The commit mentions explicitly that this issue is not fixed yet, and `ghc
 A.hs` does indeed still give rise to a panic.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13981#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
|  
Report Content as Inappropriate

Re: [GHC] #13981: Family instance consistency checks happens too early when hs-boot defined type occurs on LHS

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#13981: Family instance consistency checks happens too early when hs-boot defined
type occurs on LHS
-------------------------------------+-------------------------------------
        Reporter:  ezyang            |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.4.1
       Component:  Compiler (Type    |              Version:  8.2.1-rc2
  checker)                           |
      Resolution:                    |             Keywords:  hs-boot
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 bgamari):

 * status:  closed => new
 * resolution:  fixed =>
 * milestone:  8.2.1 => 8.4.1


Comment:

 Indeed it did. Thanks for bringing this to my attention.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13981#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
Loading...