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
#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]: 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