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
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
#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: -------------------------------------+------------------------------------- Comment (by darchon): Replying to [comment:2 goldfire]: 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. I would've found it more understandable if the reported type was `Vec (((0 + 1) + 1) + 1) a`, why is the `n` part normalised to `2`? in stead of being left `((0+1)+1)`? That was the behaviour in GHC 7.6.1: {{{ ~/devel/test$ ghci example/vec.hs GHCi, version 7.6.1: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer-gmp ... linking ... done. Loading package base ... linking ... done. [1 of 1] Compiling Main ( vec.hs, interpreted ) Ok, modules loaded: Main. *Main> :t (1:>2:>3:>Nil) (1:>2:>3:>Nil) :: Num a => Vec (((0 + 1) + 1) + 1) a }}} I was mostly confused that we started fully normalising type families in 7.8, but now suddenly in 7.10 only normalise until we reach the outermost applied type family. the original type, depending on what has fewer nodes in its AST? I think we should have: either the behaviour of 7.6.1: don't normalise, or of 7.8.3: fully normalise. I personally prefer the 7.8 behaviour (the reported type in case of using the typelits operators is smaller and more readable), especially as that already seems what we do for bound variables. Replying to [comment:3 simonpj]:
So I think our guess is that normalising is usually the Right Thing. It seems inconsistent not to do it here too. If we want to, the spot is in `TcRnDriver.tcRnExpr`. I'll have a look and see if normalising type families in `tcRnExpr` breaks anything, and then submit a patch.
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10321#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler