#12088: Type/data family instances in kind checking -------------------------------------+------------------------------------- Reporter: alexvieth | Owner: Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #11348, #12239 | Differential Rev(s): Phab:D2272 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Ah, now that makes more sense. To flesh it out slightly: * The '''declaration''' `F:sig` of a type family `F` is its kind signature, e.g. {{{ type family F a :: * -> * }}} * The '''definition''' `F:def` of a type family `F` is the collection of all its type instances (in this module). e.g. {{{ type instance F Int = Maybe type instance F Bool = [] }}} For the purposes of this conversation we treat the instances for a single type family `F` as a single "clump"; they are always treated together. * Each '''vertex''' of the dependency graph is either * the declaration `F:sig` (i.e. kind signature) of a type family `F`, or * the definition `F:def` (i.e. type instances) of the type family. * If there is an '''edge''' in the graph from A to B, then A depends on B, and B must be type-checked before A. * The edges are as follows * An edge from `F:def` to `F:sig` * An edge from `F:sig` to `G:sig`, '''and from `F:def` to `G:def`,''' for any tycon `G` syntactically mentioned in `F`'s declaration * An edge from `F:def` to `G:def` for any tycon `G` syntactically mentioned in `G`'s definition. Now do strongly connected component analsis and process in order. Richard's magic is in the bold part of the second bullet. We could do with a proof of some kind. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12088#comment:37 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler