#12239: Dependent type family does not reduce -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies 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 goldfire): This is annoying to fix but I don't think will require any great engineering feats. The be clear, the problem is to convert a type `forall (a :: F x). blah` to `forall (b :: s). blah[a |-> b |> co]`, where `s` is the flattened form of `F x` (either an fuv or some other type) and `co :: s ~ F x`. Here's the approach I have in mind: include a `TCvSubst` in `FlattenEnv`. Whenever the kind of a bound type variable is flattened, extend the substitution to map the original variable (that is, `a`) to a new one `b` (with a fresh unique -- use `uniqAway`) that has the flattened kind (and is casted, as above). This substitution must be applied over the entire scope of the bound variable (the `blah` in our example). But it would be inefficient just to apply the substitution, so we consult this substitution in `flattenTyVar` as appropriate. Specifically, I think we would need to update the first case in `flatten_tyvar1`, which deals with non-`TcTyVar`s -- that is, locally bound variables. Does this sound like something you might tackle? I'm sure bumps will come up along the road, but if you're feeling like getting your hands dirty here, I can continue to advise. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12239#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler