#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