[GHC] #10321: GHC.TypeLits.Nat types no longer fully simplified.
#10321: GHC.TypeLits.Nat types no longer fully simplified. -------------------------------------+------------------------------------- Reporter: darchon | Owner: Type: bug | Status: new Priority: normal | Milestone: 7.10.2 Component: Compiler | Version: 7.10.1 (Type checker) | Operating System: Unknown/Multiple Keywords: TypeLits | Type of failure: Other Architecture: | Blocked By: Unknown/Multiple | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10321 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10321: GHC.TypeLits.Nat types no longer fully simplified. -------------------------------------+------------------------------------- Reporter: darchon | Owner: Type: bug | Status: new 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 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 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10321#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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 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` -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10321#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10321#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
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
#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 adamgundry): * cc: adamgundry (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10321#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 Richard Eisenberg
#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: | ghci/scripts/T10321 Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by simonpj): * testcase: => ghci/scripts/T10321 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10321#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | ghci/scripts/T10321 Related Tickets: | Blocking: | Differential Revisions: phab:D870 -------------------------------------+------------------------------------- Changes (by darchon): * differential: => phab:D870 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10321#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10321: GHC.TypeLits.Nat types no longer fully simplified. -------------------------------------+------------------------------------- Reporter: darchon | Owner: Type: bug | Status: new Priority: highest | 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: | ghci/scripts/T10321 Related Tickets: | Blocking: | Differential Revisions: phab:D870 -------------------------------------+------------------------------------- Changes (by simonpj): * priority: normal => highest * status: infoneeded => new Comment: Austin, can you land this please? Thanks Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10321#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10321: GHC.TypeLits.Nat types no longer fully simplified. -------------------------------------+------------------------------------- Reporter: darchon | Owner: Type: bug | Status: patch Priority: highest | 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: | ghci/scripts/T10321 Related Tickets: | Blocking: | Differential Revisions: phab:D870 -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => patch -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10321#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10321: GHC.TypeLits.Nat types no longer fully simplified.
-------------------------------------+-------------------------------------
Reporter: darchon | Owner:
Type: bug | Status: patch
Priority: highest | 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: | ghci/scripts/T10321
Related Tickets: | Blocking:
| Differential Revisions: phab:D870
-------------------------------------+-------------------------------------
Comment (by Austin Seipp
#10321: GHC.TypeLits.Nat types no longer fully simplified. -------------------------------------+------------------------------------- Reporter: darchon | Owner: Type: bug | Status: merge Priority: highest | 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: | ghci/scripts/T10321 Related Tickets: | Blocking: | Differential Revisions: phab:D870 -------------------------------------+------------------------------------- Changes (by thoughtpolice): * status: patch => merge -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10321#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10321: GHC.TypeLits.Nat types no longer fully simplified. -------------------------------------+------------------------------------- Reporter: darchon | Owner: Type: bug | Status: closed Priority: highest | Milestone: 7.10.2 Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: TypeLits Resolution: fixed | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | ghci/scripts/T10321 Related Tickets: | Blocking: | Differential Revisions: phab:D870 -------------------------------------+------------------------------------- Changes (by thoughtpolice): * status: merge => closed * resolution: => fixed Comment: Merged to `ghc-7.10`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10321#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC