[GHC] #12564: Type family in type pattern kind

[GHC]

#12564: Type family in type pattern kind
-------------------------------------+-------------------------------------
        Reporter:  int-index         |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.4.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:  14119             |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 I have an approach here worth documenting. In brief: flatten equations'
 left-hand sides, emitting constraints during reduction.

 Here is how the example in the OP would work. Original equation:

 {{{#!hs
   At (x ': _) FZ = x
 }}}

 with implicit things made explicit:

 {{{#!hs
   At @a ((:) @a x _1) (FZ @(Len @a _1)) = x
 }}}

 But now, we ''flatten''. By this, I mean we take all type family
 applications on the LHS and convert them into variables, and assert
 equality constraints that the variables equal the original type family
 applications. To wit:

 {{{#!hs
   (m ~ Len @a _1) => At @a ((:) @a x _1) (FZ @m) = x
 }}}

 This yields a ''constrained'' type family equation. (Note: this is mostly
 unrelated to
 [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1075&context=compsci_pubs
 Constrained Type Families]) During reduction, this equation would match a
 target regardless of the (implicit) argument to `FZ`, but the matcher
 would then emit a constraint asserting that this argument equals `Len @a
 _1`. It's quite like how class instance matching works: we match against
 the head, emitting any instance constraints.

 Type family equations give rise to axioms in Core. To keep type safety, we
 would need these axioms to take the evidence of the equality match as
 arguments. Continuing our example, we would get this axiom:

 {{{
 axAt :: forall (a :: Type) (x :: a) (_1 :: [a]) (m :: Nat).
         forall (cv :: m ~ Len @a _1).
         At @a ((:) @a x _1) (FZ @m) ~ x
 }}}

 Note that there are two `forall`s: the first binds type variables and the
 second binds coercion variables. In this case, the coercion variable `cv`
 is unused in the RHS, but it might potentially be mentioned.

 This equation could be used to reduce `At ["a", "b", "c"] FZ` to `"a"`. We
 would use the instantiated axiom

 {{{
 axAt Symbol "a" ["b", "c"] 2 coLen :: At ["a", "b", "c"] FZ ~ "a"
 }}}

 where `coLen :: 2 ~ Len ["b", "c"]` is built from the axioms that describe
 the behavior of `Len`.

 Note that there is already some infrastructure for this: the `cvs` in
 `CoAxBranch` (and a few other places nearby) are exactly these coercion
 variables. What's remaining to do is to perform the flattening pass that
 inserts the cvs and to teach the type-family reduction mechanism (in
 `TcFlatten`) to emit the constraints. One challenge is that sometimes
 (`normaliseType`) we reduce type families without the ability to solve
 constraints, so some care must be taken there. However, these cases are
 outside our usual pipeline and can be special-cased. (While implementing
 `-XTypeInType`, I did this once upon a time, so I know it's possible.)

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12564#comment:13>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler