#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