[GHC] #11348: Local open type families instances ignored during type checking

[GHC]

#11348: Local open type families instances ignored during type checking
-------------------------------------+-------------------------------------
        Reporter:  alexvieth         |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1-rc1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 You are so productive!  But before generating a big patch, let's agree the
 design and approach.

 Thanks for comment:4; I think I get it now.  Here's another way to say it;
 see if you agree.

 * When kind-checking a type declaration, we must obviously first check the
 declarations of any types it mentions.  E.g.
 {{{
 type S = Int
 type T = S -> S
 }}}
   We must kind-check `S` before `T` because `T` mentions `S`.

 * But we may also need to check a `type instance` declaration:
 {{{
 type family F (a :: k) :: Type
 type instance F Int = Bool

 data K a = MK (F Int)
 type R = MK 'True
 }}}
   In the declaration of `R`, the (promoted) data constructor `MK` is given
 an argument of kind `Bool`, but it expects one of kind `F Int`.  Things
 only work if we have processed the `type instance` declaration first.

 * Alas, there is no ''explicit'' dependency of the declaration of `R` on
 the `type instance` declaration.  Indeed we might also have
 {{{
 type instance F R = ...blah...
 }}}
   and we can't check ''that'' instance until after dealing with `R`.

 * Bottom line: we have to interleave processing of type/class decls with
 processing of `type instance` decls.

 So I think the algorithm must be this: '''always process a `type instance`
 declaration as soon as all the type constructors it mentions have been
 kind-checked'''.

 Algorithmically, we can't just add the `type instance` declarations to the
 strongly-connected component analysis for type/class decls, because of the
 lack of explicit dependencies.  I think we have to

 * Do SCC on the type and class declarations as now
 * Keep in hand the set of un-processed `type instance` declarations
 * Before doing a type/class SCC, first process all the `type instance`
 decls whose free vars are imported, or are now bound in the type
 environment.
 * That results in a depleted set of un-processed `type instance`
 declarations.

 Does that sound right?  Is it what your patch does?

 Incidentally this couldn't happen before `TypeInType` because previously
 we didn't promote data types like `K`.
 {{{
 Foo.hs:9:10:
     Data constructor ‘MK’ comes from an un-promotable type ‘K’
     In the type ‘MK True’
 }}}

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