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

[GHC]

#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