[GHC] #12432: TypeInType: open type family application as type family return kind fails to compile

[GHC]

#12432: TypeInType: open type family application as type family return kind fails
to compile
-------------------------------------+-------------------------------------
        Reporter:  j6carey           |                Owner:
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:  duplicate         |             Keywords:
Operating System:  Linux             |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by j6carey):

 Because of a workaround (as mentioned below), I don't have a compelling
 use case at present.

 The application I had in mind is illustrated by the recently-added
 attachment, "Test4.hs".  The idea is that you have types that express
 formulas for values, and these can be evaluated in the context of various
 run-time parameters, though for brevity I have omitted the type
 expressions whose values actually depend on run-time parameters.  Because
 some of these expressions will determine the sizes of certain objects in
 memory, I would like optimize length checks by computing static bounds on
 the range of sizes that a given type expression might specify.  In
 particular, the expression might be a constant of kind "Nat".

 The associated type family exhibiting the problem is the one that computes
 the static bounds for the values associated with type expressions.  The
 straightforward instance definition for constants of kind 'Nat' triggers
 the problem.  On the other hand, I have managed to work around the issue
 by using a helper type family; please see the comment about
 'EvalSingleton'.

 (Minor detail: this excerpt is missing certain features such as checking
 that the 'Nat' is in bounds, and recovering in some fashion, such as
 forcing it into the bounds or triggering a compilation error.  This is
 still just a toy example, though hopefully more illustrative of the
 intended use case.)

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