#12088: Promote data family instance constructors -------------------------------------+------------------------------------- Reporter: alexvieth | Owner: Type: feature request | Status: new Priority: normal | Milestone: 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 | Differential Rev(s): Phab:D2272 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Some thoughts, after discussion with my son Michael. * This entire problem arises only because of ''open'' type families; I think closed type families are fine. We could simply ban the use of open type families in the kind signature of an open type family. Or possibly all type families, I'm not sure. * Another idea: when we have a group of `type instance` decls, suppose we kind check them, but do not yet solve the kind equalities that arise; but add them to the instance environment anyway. Now solve all the kind equalities. In our example, we'd add both instances for `Open1` and `Open2` before trying to solve their kind equalities. Seems a bit scary somehow. * Question: how do dependently typed languages deal with this? For example, what if typechecking the defintion of a function `f` requires the type checker to evaluate calls to `f`? In Haskell-land you could imagine {{{ type family Id (a :: *) :: Id * }}} We reject this at the moment, but the idea is to get into a situation where, before having typechecked `f` we need to evaluate `f`. That's rather like the situation with `Open1/2`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12088#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler