Opened 3 years ago

Closed 3 years ago

#10321 closed bug (fixed)

GHC.TypeLits.Nat types no longer fully simplified.

Reported by: darchon Owned by:
Priority: highest Milestone: 7.10.2
Component: Compiler (Type checker) Version: 7.10.1
Keywords: TypeLits Cc: adamgundry
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Other Test Case: ghci/scripts/T10321
Blocked By: Blocking:
Related Tickets: Differential Rev(s): phab:D870
Wiki Page:

Description

The following code:

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE GADTs          #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators  #-}

import GHC.TypeLits

data Vec :: Nat -> * -> * where
  Nil  :: Vec 0 a
  (:>) :: a -> Vec n a -> Vec (n + 1) a

infixr 5 :>

when loaded in GHCi 7.8.3, and asking for the type of (1 :> 2 :> 3 :> Nil), gives:

$ ghci example/vec.hs 
GHCi, version 7.8.3: 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             ( example/vec.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t (3:>4:>5:>Nil)
(3:>4:>5:>Nil) :: Num a => Vec 3 a

while in GHCi 7.10.1 it gives:

$ ghci example/vec.hs 
GHCi, version 7.10.1: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( example/vec.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t (3:>4:>5:>Nil)
(3:>4:>5:>Nil) :: Num a => Vec (2 + 1) a

That is, the type-level computation, ((0 + 1) + 1) + 1 is only simplified to 2 + 1 in GHC 7.10.1, whereas in 7.8.3 2+1 was further simplified to 3.

The same still happens in HEAD (20150417)

$ ghci example/vec.hs 
GHCi, version 7.11.20150417: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( example/vec.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t (3:>4:>5:>Nil)
(3:>4:>5:>Nil) :: Num a => Vec (2 + 1) a

I strongly feel that the behaviour in ghc 7.8.3 is the desired behaviour.

Change History (14)

comment:1 Changed 3 years ago by rwbarton

I think the behavior of when to expand/simplify type families may have changed intentionally in 7.10, but simplifying the type only as far as Num a => Vec (2 + 1) a certainly looks weird.

I also note that the behavior is different if the value is first bound to a variable:

*Main> let x = (3:>4:>5:>Nil)
*Main> :t x
x :: Num a => Vec 3 a

comment:2 Changed 3 years ago by goldfire

Status: newinfoneeded

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!

comment:3 Changed 3 years ago by simonpj

I looked at this too. Turns out that we do normalise types for inferred let-bindings; see line 661 of TcBinds, the call to normaliseType in mkInferredPolyId. The explanation there is "to make the type as simple as possible". See commit a6e7654b. It doesn't mention a Trac ticket.

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

comment:4 Changed 3 years ago by goldfire

But yet we take (significant) pains not to look through type synonyms when reporting errors... we even avoid looking through type synonyms when normalizing!

So, is the general idea that vanilla type synonyms are preferred over their RHSs, but reducing type families is better than leaving them unreduced? Perhaps. I have no objection to this. It is a little odd that changing a vanilla type synonym to a closed type family with one (universal) equation would change behavior, but this is all pretty-printing and heuristic anyway, so that's not too bad.

comment:5 in reply to:  2 Changed 3 years ago by darchon

Replying to goldfire:

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.

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.

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?

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 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.

comment:6 Changed 3 years ago by adamgundry

Cc: adamgundry added

comment:7 Changed 3 years ago by Richard Eisenberg <eir@…>

In d4cf5591e51e2b91b3877a05f8153db1f5328994/ghc:

Test #10321 in ghci/scripts/T10321

comment:8 Changed 3 years ago by simonpj

Test Case: ghci/scripts/T10321

comment:9 Changed 3 years ago by darchon

Differential Rev(s): ​phab:D870

comment:10 Changed 3 years ago by simonpj

Priority: normalhighest
Status: infoneedednew

Austin, can you land this please?

Thanks

Simon

comment:11 Changed 3 years ago by simonpj

Status: newpatch

comment:12 Changed 3 years ago by Austin Seipp <austin@…>

In f7daf5afe2ba4f60f60245fa82306b89a272ffa8/ghc:

Normalise type families in the type of an expression

Before, the type of an expression, and the type of a variable
binding that expression used to be different in GHCi. The
reason being that types of bound variables were already normalised.
Now, both are normalised.

This implements the suggestions as given in Trac #10321
Also adds an expected output for test T10321

Reviewed By: goldfire, simonpj

Differential Revision: https://phabricator.haskell.org/D870

GHC Trac Issues: #10321

comment:13 Changed 3 years ago by thoughtpolice

Status: patchmerge

comment:14 Changed 3 years ago by thoughtpolice

Resolution: fixed
Status: mergeclosed

Merged to ghc-7.10.

Note: See TracTickets for help on using tickets.