I don't really understand your suggestion Richard.
Firstly, we often infer the kind of a data type, so it's hard to separate dependence on its kind from dependendence on its definition. I din't undersand the precise dependency analysis that you informally
#12088: Promote data family instance constructors -------------------------------------+------------------------------------- Reporter: alexvieth | Owner: Type: feature request | Status: new Priority: normal | Milestone: 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 | Differential Rev(s): Phab:D2272 Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:14 simonpj]: propose. Yes, of course. But I think this is easily dispatched: if we are inferring the kind, then use this rule: * If a datatype's definition depends on the definition of `X`, then its type depends on the type of `X`. I haven't dwelt on this very long, but that seems to capture the nature of types that can be inferred. Here is something toward a specification of my idea: 1. In a datatype definition for `T`: a. Let `X` be a tycon mentioned in `T`'s kind signature or in kind signatures of type variables to `T`. Then `T`'s type depends on `X`'s type and `T`'s definition depends on `X`'s definition. b. Let `K` be a datacon mentioned in `T`'s kind signature or in kind signatures of type variables to `T`. Let `S` be the tycon containing `K`. (`S` might be a data family ''instance'' tycon, too.) Then `T`'s type depends on the definition of `S`. c. Let `X` be a tycon mentioned in the type signature of a datacon in `T`. Then the definition of `T` depends on the type of `X`. In addition, if `T` does not have CUSK, then the type of `T` depends on the type of `X`. d. Let `K` be a datacon (belonging to tycon `S`) mentioned in the type signature of a datacon in `T`. Then the definition of `T` depends on the definition of `S`. In addition, if `T` does not have a CUSK, then the type of `T` depends on the type of `S`. (If `S` is a data family instance tycon, then this last sentence refers to the family for `S`, not the instance tycon, which has no type declaration to depend on.) 2. In a closed type family definition for `C`: a. Let `X` be a tycon mentioned in any kind signature in the head of `C`. Then `C`'s type depends on `X`'s type and `C`'s definition depends on `X`'s definition. b. Let `K` be a datacon (belonging to tycon `S`) mentioned in any kind signature in the head of `C`. Then `C`'s type depends on `X`'s definition. c. Let `X` be a tycon mentioned in any equation for `C`. Then `C`'s definition depends on `X`'s type. In addition, if `C` does not have a CUSK, then `C`'s type depends on `X`s type. d. Let `K` be a datacon (belonging to tycon `S`) mentioned in any equation for `C`. Then `C`'s definition depends on `S`'s definition. In addition, if `C` does not have a CUSK, then `C`'s type depends on `S`'s type. (Or `S`'s family's type, as above.) 3. In the declaration of an open type family `F`: a. Let `X` be a tycon mentioned in any kind signature in the declaration for `F`. Then `F`'s type depends on `X`'s type and `F`'s instance block depends on `X`'s definition. b. Let `K` be a datacon (belonging to tycon `S`) mentioned in the declaration for `F`. then `F`'s type depends on `S`'s type and `F`'s instance block depends on `S`'s definition. 4. In a type family instance for `F`: a. Let `X` by a tycon mentioned in the instance. Then `F`'s instance block depends on `X`'s type. b. Let `K` be a datacon (belonging to tycon `S`) mentioned in the instance. Then `F`'s instance block depends on `S`'s definition. 5. In the declaration of an open data family `D`: a. Let `X` be a tycon mentioned in any kind signature in the declaration for `D`. Then `D`'s type depends on `X`'s type. b. Let `K` be a datacon (belonging to tycon `S`) mentioned in the declaration for `D`. then `D`'s type depends on `S`'s type. 6. In the declaration of a data instance: as for a regular datatype, where the kind signatures are inherited from the data family declaration. Left for another time: classes. Question raised: Data families always have a CUSK because a data family is always open. But might a data family instance ''not'' have a CUSK? What happens then? Perhaps we need to have CUSK analysis on data family instances, too.
Secondly, I think that open type families are indeed the odd one out, as
you acknowledge in the "odd conundrum". I don't see what's gained by separating types from defns even if we could. We gain induction recursion, #11962. Even before this whole discussion, I had the general idea of this separation. See [wiki:DependentHaskell/Internal#Separatingtypesignaturesfromdefinitions this wiki page], written some time ago, on this idea.
Thirdly, you suggest kind-checking all equations for a type family
together as a single group. But you can't do that if they mention data types that have not yet been defined. Yet we can't delay too long ... getting those instances into play early is the whole point. It's true that my approach will sometimes fail when a finer-grained approach would succeed. But I don't think we're trying to get ''every'' use case. We're trying to get a predictable approach that works just about all the time. Here is an example that would fail: {{{ type family F a = r | r -> a data T :: F a -> Type where MkT :: T False type instance F Int = Bool type instance F Char = Proxy MkT }}} The definition of `T` depends on the first instance while the second instance depends on the definition of `T`. I'm not bothered rejecting this.
Fourth, the dependence may be indirect. In the example, Open2 mentions
Open1 directly. But it could instead mention F directly, where F is an open family that has an equation like `type instance F [t] = Open1 t`. Now the dependence on Open1 is hidden.
Isn't this just transitivity? Depending on the "definition" of a type family means dependency on the block of instances -- all of them. So anything an instance depends on is transitively reachable. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12088#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler