[GHC] #12239: Dependent type family does not reduce

[GHC]

#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