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

 Sorry for the delay, new contract is keeping my occupied. comment:17
 certainly shows a shortcoming in the patch for #11348. No sense reopening
 it though, this ticket can supersede it (its summary could use a revision
 for scope). Thanks for the wiki writeup mpickering. It's accurate and I
 have nothing to add right now. That section called "The Solution" is a
 tall order!

 Replying to [comment:20 goldfire]:

 > This would then put ill-kinded equalities into the context. I think it
 would be awfully hard to avoid getting GHC to loop or do other silly
 things with a bad context. Perhaps you could squeeze this through, but I'm
 very skeptical.
 >
 > Or am I misunderstanding something?

 You're probably not misunderstanding. I'm just sounding off ideas and I'm
 no expert on GHC's type checker. Putting ill-kinded equalities into the
 context sounds irresponsible yes, but they'll all be of the form `F k ~ l`
 for some open type family `F` (or similar for higher arities). Does this
 fact help at all? Could you come up with a case where an ill-kinded
 equality of this form would wreak havoc?

 How about a variation on that suggestion of mine? A kind of lazy
 evaluation for open type families in kinds. While type checking other
 declarations, rather than assuming the (possibly ill-kinded) equalities
 arising from open type families to be true, defer them until after all
 declarations are checked. Then we end up with a set of equalities
 featuring open type family constructors which must be solved using all
 open type family instances. So in the `FieldCount` example from
 comment:17, repeated here for convenience:

 {{{#!hs
 {-# LANGUAGE TypeInType, GADTs, TypeFamilies #-}

 import Data.Kind (Type)

 data N = Z | S N

 data Fin :: N -> Type where
   FZ :: Fin (S n)
   FS :: Fin n -> Fin (S n)

 type family FieldCount (t :: Type) :: N

 type family FieldType (t :: Type) (i :: Fin (FieldCount t)) :: Type

 data T

 type instance FieldCount T = S (S (S Z))

 type instance FieldType T FZ = Int
 type instance FieldType T (FS FZ) = Bool
 type instance FieldType T (FS (FS FZ)) = String
 }}}

 The only declarations which give rise to a deferred kind equality are the
 `FieldType` instances.

 - `type instance FieldType T FZ = Int` yields `S n0 ~ FieldCount T`
 - `type instance FieldType T (FS FZ) = Bool` yields `S (S n1) ~ FieldCount
 T`
 - `type instance FieldType T (FS (FS FZ)) = String` yields `S (S (S n2)) ~
 FieldCount T`

 These don't stop type checking dead, they're just tucked away for later
 and `type instance FieldCount T = S (S (S Z))` will eventually be checked
 (either before or after, we don't care) and available when those three
 equalities are solved. The program will therefore pass: `n0 := (S (S Z))`,
 `n1 := S Z`, `n2 := Z`.

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