#5296 closed feature request (fixed)
Add explicit type applications
Reported by: | dsf | Owned by: | goldfire |
---|---|---|---|
Priority: | low | Milestone: | 8.0.1 |
Component: | Compiler (Type checker) | Version: | 7.0.3 |
Keywords: | Cc: | dsf@…, hackage.haskell.org@…, sweirich@…, mail@…, steven.keuchel@…, hamidhasan14@…, jstolarek, wren@… | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | typecheck/should_compile/Vta{1,2} typecheck/should_fail/VtaFail |
Blocked By: | #1897 | Blocking: | #10770 |
Related Tickets: | #4466 | Differential Rev(s): | Phab:D1681 |
Wiki Page: |
Description
This example is derived from code in my application. It works, but I can't add a signature to it. In other places it is preventing some code from compiling at all.
{-# LANGUAGE KindSignatures, MultiParamTypeClasses, RankNTypes #-} {-# OPTIONS -Wall #-} module Test where class C t1 t2 m where method :: Int -> m t2 f :: forall t1 t2 (m :: * -> *). C t1 t2 m => Int -> m t2 f x = method x
Change History (30)
comment:1 in reply to: ↑ description Changed 5 years ago by dsf
comment:2 Changed 5 years ago by dsf
- Blocked By 1897 added
- Cc dsf@… added
comment:3 Changed 5 years ago by liyang
- Cc hackage.haskell.org@… added
comment:4 Changed 5 years ago by igloo
- Milestone set to 7.4.1
comment:5 Changed 5 years ago by simonpj
The problem here is related to #1897, as you point out, but is even clearer because it doesn't even involve type families. The trouble is this. method has type
method :: C t1 t2 m => Int -> m t2
Notice that t1 does not appear in method's type. Now GHC is faced with
From given (C t1 t2 m) deduce wanted (C t3 t2 m)
Notice the t3. The call of method means that the second and third args of C must be t2, m; but the first can be anything. So type inference is supposed to guess what type it should use for t3. Here there is a unique choice, but in general it is hard to solve problems where there is are positive clues, only that there is just one magic solution.
If we could supply the type arguments to the call to method, we could say this:
f :: forall t1 t2 (m :: * -> *). C t1 t2 m => Int -> m t2 f x = method @t1 @t2 @m x
Here I put the type args with a leading "@" (the notation I'm currently considering for type args). Now we'd be fine.
In short, the only Decent Solution here seems to me to be explicit type arguments. Unless anyone else has better ideas.
comment:6 Changed 5 years ago by simonpj
- Summary changed from Compile succeeds without signature, but fails with the signature suggested by GHC to Add explicit type applications
- Type changed from bug to feature request
comment:7 Changed 5 years ago by simonpj
See also #4466
comment:8 Changed 4 years ago by igloo
- Milestone changed from 7.4.1 to 7.6.1
- Priority changed from normal to low
comment:9 Changed 4 years ago by igloo
- Milestone changed from 7.6.1 to 7.6.2
comment:10 Changed 3 years ago by sweirich
- Cc sweirich@… added
comment:11 Changed 3 years ago by kosmikus
- Cc mail@… added
comment:12 Changed 3 years ago by skeuchel
- Cc steven.keuchel@… added
comment:13 Changed 3 years ago by Hamidhasan
- Cc hamidhasan14@… added
- difficulty set to Project (more than a week)
comment:14 Changed 2 years ago by jstolarek
- Cc jan.stolarek@… added
comment:15 Changed 22 months ago by thoughtpolice
- Milestone changed from 7.6.2 to 7.10.1
Moving to 7.10.1.
comment:16 Changed 16 months ago by thoughtpolice
- Milestone changed from 7.10.1 to 7.12.1
Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.
comment:17 follow-up: ↓ 23 Changed 9 months ago by goldfire
- Architecture changed from x86_64 (amd64) to Unknown/Multiple
- Differential Rev(s) set to Phab:D1138
- Operating System changed from Linux to Unknown/Multiple
- Owner set to goldfire
Patch available now, at Phab:D1138 and at branch wip/type-app.
There are implementation notes in Phab. Here are some design notes:
- There is no explicit kind instantiation. It just won't parse! This will be fixed along with Phab:D808.
- The new extension TypeApplications implies AllowAmbiguousTypes. This makes sense, because in the presence of visible type application, there is really no such thing as an ambiguous type.
- Suppose there is no Eq instance for T and a,b :: T. The expression a == b is clearly ill-typed. Previously, the error was reported on the ==. Now it's reported on the whole expression. I think this makes sense.
I have two open design questions:
- What to do with :type in GHCi? Suppose we have pair :: forall a. a -> forall b. b -> (a,b). I ask :type pair 3. The real type of this expression is forall b. b -> (a0, b), where a0 is the type of the overloaded 3. The problem is that this type loses the fact that we need Num a0. We could say forall b. Num a0 => b -> (a0, b), which is a little closer. Would we report that without -fprint-explicit-foralls? It would be wrong to say forall a b. Num a => b -> (a, b) (as is done today, even with this patch) because we can't instantiate a with a further visible type application.
- It would be nice to be able to say 3 @Int instead of (3 :: Int). But this doesn't work out. Writing 3 in code really means fromInteger $3 (where $3 is the internal representation for the Integer 3). fromInteger comes from the Num class; it has type forall a. Num a => Integer -> a. So, we would want 3 @Int to really become fromInteger @Int $3. But this is hard to arrange for. Alternatively, we could change fromInteger to have type Integer -> forall a. Num a => a, which would work swimmingly. But we can't do this, because class methods always have their class variables quantified first. Making this change would mean writing a wrapper around fromInteger:
fromIntegerVta :: Integer -> forall a. Num a => a fromIntegerVta = fromInteger
Interpreting overloaded numbers in Haskell source would then use fromIntegerVta. But this is all a little painful. Is it worth it to have 3 @Int?
comment:18 follow-up: ↓ 19 Changed 9 months ago by simonpj
Can I tell, in GHCi, whether a particular function (perhaps in scope by being imported) is amenably to VTA? Perhaps :info f tells me?
For (2) I suggest just saying (3 :: Int). There are more exciting things to do than allow "@" in place of "::".
comment:19 in reply to: ↑ 18 Changed 9 months ago by goldfire
Replying to simonpj:
Can I tell, in GHCi, whether a particular function (perhaps in scope by being imported) is amenably to VTA? Perhaps :info f tells me?
No. But there should be. :info would be easy to modify. But I think :type should indicate this as well somehow.
For (2) I suggest just saying (3 :: Int). There are more exciting things to do than allow "@" in place of "::".
Yes, I suppose that's true.
comment:20 Changed 8 months ago by thoughtpolice
- Milestone changed from 7.12.1 to 8.0.1
Milestone renamed
comment:21 Changed 7 months ago by jstolarek
- Cc jstolarek added; jan.stolarek@… removed
comment:22 Changed 7 months ago by WrenThornton
- Cc wren@… added
comment:23 in reply to: ↑ 17 Changed 7 months ago by WrenThornton
Replying to goldfire:
I have two open design questions:
- What to do with :type in GHCi? Suppose we have pair :: forall a. a -> forall b. b -> (a,b). I ask :type pair 3. The real type of this expression is forall b. b -> (a0, b), where a0 is the type of the overloaded 3. The problem is that this type loses the fact that we need Num a0. We could say forall b. Num a0 => b -> (a0, b), which is a little closer. Would we report that without -fprint-explicit-foralls? It would be wrong to say forall a b. Num a => b -> (a, b) (as is done today, even with this patch) because we can't instantiate a with a further visible type application.
IMO, the type forall a b. Num a => b -> (a, b) is wrong for the expression (pair 3) aka (pair @a (fromInteger @a $3)), because the type a is fixed, albeit unknown. My first inclination would be to say those expressions have type iota a. Num a => forall b. b -> (a, b). Of course, I wouldn't expect most folks to know anything about the iota quantifier, so I probably wouldn't print it that way. Do we have a notation for metavariables yet? We could say Num ?a => forall b. b -> (?a, b) supposing ?a is the way we write a metavariable (rather than that syntax being used by ImplicitParams).
- It would be nice to be able to say 3 @Int instead of (3 :: Int).
I agree with spj here. There's not really any benefit in terms of expressibility nor brevity.
comment:24 Changed 7 months ago by goldfire
Thanks for the suggestion. Unfortunately, I think that ?a looks too much like ImplicitParams. But I do like the general idea.
Here's a very, very radical thought: what if we use color? We could print forall b. Num a => b -> (a, b) but put a in a different color. (Even though it's a bit of a lie, I prefer putting the forall b before the Num a, only because Haskellers are much more used to that ordering.) Non-colored terminals still get all the information they need: that b is available for type application whereas a is not. But someone with color could see the needed information very easily.
But something tells me it would be a major plumbing job to get color output... :(
comment:25 Changed 7 months ago by goldfire
- Blocking 10770 added
comment:26 Changed 4 months ago by goldfire
- Differential Rev(s) changed from Phab:D1138 to Phab:D1681
comment:27 Changed 4 months ago by Richard Eisenberg <eir@…>
In 2db18b81/ghc:
comment:28 Changed 4 months ago by goldfire
- Resolution set to fixed
- Status changed from new to closed
- Test Case set to typecheck/should_compile/Vta{1,2} typecheck/should_fail/VtaFail
All set now.
comment:29 Changed 2 months ago by andrewthad
This might be a little too late, but I wanted to raise a question about the relationship this has with AllowAmbiguousTypes. I haven't tried it out yet, but based on an earlier comment in this thread, I think that turning on VisibleTypeApplication will also turn on AllowAmbiguousTypes. I don't think that this is necessary, and I think that there are situation where it is detrimental the library users. Let's say that I have a Rec from vinyl and I'm using rget from Data.Vinyl.Lens. Today, if I have myRec :: Rec Identity '[Char,Bool,Int], I can write rget (Proxy :: Proxy Int) myRec to get the Int value out. In the future, it may be desirable to write a function rget2 that can take the argument by VisibleTypeApplication instead. So, we would call rget2 @Int myRec instead.
Here's the issue that I'm getting at. What does an end user have to enable to be able to use rget2? At the definition site, in the case of rget2, we actually don't need AllowAmbiguousTypes, but let's pretend that we did (I should have picked a different example). When a user turns on VisibleTypeApplication to be able to use a function that will otherwise have ambiguous type variable instantiation, I don't think that they should get AllowAmbiguousTypes turned on as well. If I understand correctly, AllowAmbiguousTypes is only needed to define these functions, not to use them.
comment:30 Changed 2 months ago by goldfire
It depends on what ambiguity means. In a language with visible type application,
foo :: (Show a, Read a) => String -> String
can be called quite easily. Thus the ambiguity check seems unhelpful here. Thus the decision to have TypeApplications turn on AllowAmbiguousTypes.
I do see what you're getting at. Perhaps this is the wrong design, and I'm happy to think about changing it (although it does seem a bit late). I will say that if you do want the ambiguity check, you can always use NoAllowAmbiguousTypes.
If you wish to pursue the issue, I think a good next step is posting to ghc-devs to see what others think.
Replying to dsf:
To be clear, to get the module to load remove the signature from f. In my application I might be able to get things working by removing signatures, but it leads to a cascade of signature removal that is not really acceptable.