[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):

 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