[GHC] #10321: GHC.TypeLits.Nat types no longer fully simplified.

[GHC]

#10321: GHC.TypeLits.Nat types no longer fully simplified.
-------------------------------------+-------------------------------------
        Reporter:  darchon           |                   Owner:
            Type:  bug               |                  Status:  infoneeded
        Priority:  normal            |               Milestone:  7.10.2
       Component:  Compiler (Type    |                 Version:  7.10.1
  checker)                           |                Keywords:  TypeLits
      Resolution:                    |            Architecture:
Operating System:  Unknown/Multiple  |  Unknown/Multiple
 Type of failure:  Other             |               Test Case:
      Blocked By:                    |                Blocking:
 Related Tickets:                    |  Differential Revisions:
-------------------------------------+-------------------------------------
Changes (by goldfire):

 * status:  new => infoneeded


Comment:

 It's hard to get this right.

 Consider this example:

 {{{
 type LotsOf a = (a,a,a,a,a,a,a,a,a,a)

 data Foo a where
   MkFoo :: a -> Foo (LotsOf a)
 }}}

 If I say `:t MkFoo True`, I get `MkFoo True :: Foo (LotsOf Bool)`. That's
 better than if `LotsOf` had gotten expanded out.

 This is the same behavior as what you're seeing. GHC sees that the return
 type of `:>` is `Vec (n + 1) a`, so it figures out what `n` is and reports
 the type in the way it does. What it sounds like you want is for GHC to
 then normalize the type.

 I'm not saying that normalizing the type here is wrong, just that it's not
 always right. GHC, in general, tries not to evaluate types any more than
 it has to. In fact, upon further inspection, I'm surprised that GHC does
 what you want in the bound-variable case, or that it worked previously.

 Bottom line: can you propose a mechanism to sort this out? Simplify only
 type-lits operators? Simplify type families but not type synonyms?
 Simplify everything (this would be a big change from current behavior)?
 When printing, simplify, and print out the either the simplified type or
 the original type, depending on what has fewer nodes in its AST?

 Perhaps we can do what you want, but we need a specification of what you
 want first. Thanks!

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