[GHC] #12088: Type/data family instances in kind checking

[GHC]

#12088: Type/data family instances in kind checking
-------------------------------------+-------------------------------------
        Reporter:  alexvieth         |                Owner:
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.2.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):

 RE comment:25:

 * I have no idea how to actually implement this idea.   Type constructors,
 axioms, etc have no late-bound holes in them and it would be
 architeturally difficult to change that, becuase they are all tied
 together so they point to each other in a graph.  Difficult to update.

 * More seriously, I do not know whother the resulting system would be
 sound.  The kinding of one instance depends on executing another instance;
 and vice versat.  At at minimum I'd want to see a ''specification'' in
 langauge that a type-theory person could understand, and a sketch proof of
 soundness.

 * Stephanie Weirich and Ricahrd Eisenberg are world experts of this stuff.
 We sat down and ICFP and made zero progress.  That doesn't mean that no
 progress is possible; but it does mean that it's premature to implement
 anything until we undersatnd the theory.

 * It's important to bre able to explain to programmers exactly what will
 kind-check and what will not.  The fact that the implementation is already
 jolly tricky, and yet does not do the job, is a worry.  Making it much
 more complicated still feels wrong to me.

 Better to withdraw to something that is (a) simple to explain and (b)
 simple to implement.   That leaves a clear research challenge for some
 research student to tackle.

 > I appreciate that, at the term level, I don't need to worry about the
 order of my definitions.

 I agree.  But I don't know anything better.   If Ricahrd gets his way,
 thing will happen at the term level, when typing `f` requires executing
 `g` anf vice versa.  Except it's worse at the type level becaues of open
 type families.

 I specualte that you'll never need a phasing annotation if you only need
 closed type families.   Maybe that's why this issue doesn't show up for
 Coq, Agda etc?

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