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

4 Jan 2016

#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 alexvieth):

 > 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.

 Yes I believe this is the way forward. Your description of the problem is
 spot on, and the third bullet is particularly important.

 With my patch, all `InstDecl`s (even data and class instances) enter the
 dependency graph. Every `InstDecl` depends upon its class or family and
 the `FreeVars` determined by the renamer, while every `TyClDecl` which
 mentions a type family or class depends also upon ''every'' one of its
 instances known to the renamer. But given the third bullet point, this
 method is too coarse; `type R = MK 'True` should ''not'' depend upon `type
 instance F R`.

 > 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.

 As far as I can tell, there is enough information to add them, except when
 dealing with instances of imported families. Consider this example (from a
 note in the patch)

 {{{#!hs

 --A.hs
   type family Closed (t :: Type) :: Type where
       Closed t = Open t

   type family Open (t :: Type) :: Type

 -- B.hs
   import A

   data Q where
       Q :: Closed Bool -> Q

   type instance Open Int = Bool

   type S = 'Q 'True
 }}}

 We must ensure that `type instance Open Int = Bool` comes before `type S =
 'Q 'True`, but `'Q` doesn't depend directly upon `Open`, and we don't know
 that `Closed` depends upon `Open`! Although we add `type instance Open
 Int` to the dependency graph, we don't have enough information to connect
 it with `type S`, but this is OK so long as we fulfil the aforementioned
 goal:
 > always process a type instance declaration as soon as all the type
 constructors it mentions have been kind-checked.
 In the patch, we achieve this by doing dependency analysis in two passes
 1. Add a new "meta-node" dependent upon every `InstDecl`, and on which
 every `TyClDecl` depends.
 2. Compute SCCs of this augmented graph.
 3. For every SCC, remove the meta-node and recompute the SCC.
 4. Concatenate these SCCs.
 If an `InstDecl` does not depend upon a `TyClDecl`, then it will appear in
 an SCC of the augmented graph ''before'' the SCC in which the `TyClDecl`
 appears, thanks to the made-up dependency of the `TyClDecl` on every
 `InstDecl`.

 I'm not sure I follow your description of the algorithm. The first bullet
 says we do SCC on the `TyClDecl`s, but the third point says that before we
 do this, we must process the `InstDecl`s. Did you mean that we keep SCC as
 is, with just `TyClDecl`s, and during type-checking of the groups, we
 ensure that when an `InstDecl`s dependencies are met, we check it
 immediately? That seems simpler and less invasive than my approach, and
 doesn't suffer from the problem shown by the third bullet. But it's not
 clear to me how to efficiently determine when an `InstDecl`s dependencies
 have been met. We wouldn't want to scan the entire set each time we
 process a `TyClDecl`, no?

--
Ticket URL: 
GHC 
The Glasgow Haskell Compiler

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

tags

participants (1)