[GHC] #13060: Visible type application doesn't work for functions with inferred types
#13060: Visible type application doesn't work for functions with inferred types -------------------------------------+------------------------------------- Reporter: Feuerbach | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{ GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/feuerbach/.ghci Prelude> :set -XTypeApplications -fprint-explicit-kinds -fprint-explicit- foralls Prelude> :t id id :: forall {a}. a -> a Prelude> :t id @Int id @Int :: Int -> Int Prelude> let foo :: a -> a; foo = id Prelude> :t foo foo :: forall {a}. a -> a Prelude> :t foo @Int foo @Int :: Int -> Int Prelude> let bar = id Prelude> :t bar bar :: forall {a}. a -> a Prelude> :t bar @Int <interactive>:1:1: error: • Cannot apply expression of type ‘a0 -> a0’ to a visible type argument ‘Int’ • In the expression: bar @Int }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13060 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13060: Visible type application doesn't work for functions with inferred types -------------------------------------+------------------------------------- Reporter: Feuerbach | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): This is by design, but there are two competing elements of the design at work here: 1. We really don't want type application to work with inferred types, as doing so would be very very fragile in the general case. See Section 3 of the [http://cs.brynmawr.edu/~rae/papers/2016/type-app/visible-type-app.pdf Visible Type Applications] paper. 2. In GHC 8.0, GHCi forgets information about the distinction between specified and inferred type variables, by design. See comment:16:ticket:11376 and below. The short version is that Simon advocated for the current design (which instantiates all types and then regeneralizes), while I advocated for just reporting the type. I lost the debate, and so GHCi loses information about type variables. These two design points lead to the confusing (but correct) interaction above. The good news is that HEAD (and, therefore, GHC 8.2) will have `:type +v`, which will not instantiate. You will see that `:type +v id` reports `forall a. a -> a` and `:type +v bar` reports `forall {a}. a -> a`, making the difference between these types clear(er). To be honest, I'm not sure if there's any way to make this clearer to users, who are understandably befuddled by your interaction. (Hence my standpoint in the debate in the commentary on #11376.) Concrete suggestions are very welcome. Otherwise, feel free to close the ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13060#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13060: Visible type application doesn't work for functions with inferred types -------------------------------------+------------------------------------- Reporter: Feuerbach | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Feuerbach): * status: new => closed * resolution: => invalid Comment: Thanks Richard, this makes sense. I agree that depending on the inferred order of type variables in actual code would be a bad idea. In my case, I was just trying to evaluate something quickly in ghci like this: {{{ *Main> description decoGrid <interactive>:64:1: error: • Ambiguous type variable ‘a0’ arising from a use of ‘description’ prevents the constraint ‘(LayoutModifier (Decoration DefaultDecoration DefaultShrinker) a0)’ from being solved. Probable fix: use a type annotation to specify what ‘a0’ should be. These potential instance exist: one instance involving out-of-scope types (use -fprint-potential-instances to see them all) • In the expression: description decoGrid In an equation for ‘it’: it = description decoGrid <interactive>:64:13: error: • Ambiguous type variable ‘a0’ arising from a use of ‘decoGrid’ prevents the constraint ‘(Eq a0)’ from being solved. Probable fix: use a type annotation to specify what ‘a0’ should be. These potential instances exist: instance Eq XEvent -- Defined in ‘Graphics.X11.Xlib.Event’ instance Eq FontSet -- Defined in ‘Graphics.X11.Xlib.Extras’ instance Eq FontStruct -- Defined in ‘Graphics.X11.Xlib.Font’ ...plus 61 others ...plus 138 instances involving out-of-scope types (use -fprint-potential-instances to see them all) • In the first argument of ‘description’, namely ‘decoGrid’ In the expression: description decoGrid In an equation for ‘it’: it = description decoGrid *Main> :t decoGrid decoGrid :: forall {a}. Eq a => ModifiedLayout (Decoration DefaultDecoration DefaultShrinker) Grid a *Main> -- ok, so I need to apply decoGrid to the right type param *Main> description (decoGrid @Window) <interactive>:67:14: error: • Cannot apply expression of type ‘ModifiedLayout (Decoration DefaultDecoration DefaultShrinker) Grid a0’ to a visible type argument ‘Window’ • In the first argument of ‘description’, namely ‘(decoGrid @Window)’ In the expression: description (decoGrid @Window) In an equation for ‘it’: it = description (decoGrid @Window) *Main> -- this works: *Main> :set -XPartialTypeSignatures -Wno-partial-type-signatures *Main> description (decoGrid :: _ Window) "DefaultDecoration Grid" }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13060#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13060: Visible type application doesn't work for functions with inferred types -------------------------------------+------------------------------------- Reporter: Feuerbach | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): Well (I don't know whether this is documented anywhere but) that should not be the confusing part--`forall {a}.` means you can't use a type application to specify the type. The confusing part is the behavior of `:t id` and `:t foo`. But `:info` will show you the difference. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13060#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC