#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): I had a good conversation with Richard and Stepanie about this ticket. Our conclusions. * Alex's cunning examples demonstrate that it's very difficult (perhaps impossible) to come up with a dependency analysis that always does the Right Thing. Even if it's possible we should not do it because (a) it'd be hard to implement and (b) it'd be extremely hard to explain exactly which programs should be OK. * Bottom line. Instead of getting in deeper, pull back. Do somthing that is simple to explain, predicatable, and simple to implement, even if it' a little less convenient. * Richard's long remarks in comment:15 actually relate to somethiug rather different called (I think) "induction recursion". It is cool but it should have a separate ticket. Richard can you do that? '''Proposal''' Get the programmer to do "phasing" explicitly if it is necessary. Specifically * Introduce a top-level '''binding separator''', thus {{{ f x = x + 1 ============ g x = f x }}} The `==========` is the binding separator. * Concrete syntax to be decided. But we have this very thing already, thus {{{ f x = x+1 $([d| |]) -- Empty Template Haskell top level splice g x = f x }}} New concrete syntax is just to make it less wierd. * Semantics. Everything before the separator is renamed and typechecked before anything after. * When typechecking data/class/instance decls, we revert to something close to the situation before Alex's patch: 1. `class`, `type`, `data`, and `data instance` declarations are SCCd and typechecked in order 2. When that is complete typecheck class `instance` and `type instance` declarations. Note that `data instance` decls come in the first wave (addressing the example in the Description), but the slippery `type instance` declarations happen only afterwards * I think we could perhaps include ''closed'' type families in step (1); c.f. comment:12. Not certain. In Alex's example in comment:8 the `type instance F` would happen last, which would fail (consistently so). To fix it, use a separator: {{{ module B where import Data.Kind import A data Q data family F (t :: Type) :: Closed t -> Type type instance Open Q = Bool ============ -- The separator ensures that data instance F Q r is -- typechecked after the type instance Open Q data instance F Q r where F0 :: F Q 'True }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12088#comment:28 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler