Opened 4 years ago
Last modified 4 weeks ago
#5296 new feature request
Add explicit type applications
Reported by: | dsf | Owned by: | goldfire |
---|---|---|---|
Priority: | low | Milestone: | 7.12.1 |
Component: | Compiler (Type checker) | Version: | 7.0.3 |
Keywords: | Cc: | dsf@…, hackage.haskell.org@…, sweirich@…, mail@…, steven.keuchel@…, hamidhasan14@…, jan.stolarek@… | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | |
Blocked By: | #1897 | Blocking: | |
Related Tickets: | Differential Revisions: | Phab:D1138 |
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 (19)
comment:1 in reply to: ↑ description Changed 4 years ago by dsf
comment:2 Changed 4 years ago by dsf
- Blocked By 1897 added
- Cc dsf@… added
comment:3 Changed 4 years ago by liyang
- Cc hackage.haskell.org@… added
comment:4 Changed 4 years ago by igloo
- Milestone set to 7.4.1
comment:5 Changed 4 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 4 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 4 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 3 years ago by igloo
- Milestone changed from 7.6.1 to 7.6.2
comment:10 Changed 2 years ago by sweirich
- Cc sweirich@… added
comment:11 Changed 2 years ago by kosmikus
- Cc mail@… added
comment:12 Changed 2 years ago by skeuchel
- Cc steven.keuchel@… added
comment:13 Changed 2 years ago by Hamidhasan
- Cc hamidhasan14@… added
- difficulty set to Project (more than a week)
comment:14 Changed 20 months ago by jstolarek
- Cc jan.stolarek@… added
comment:15 Changed 14 months ago by thoughtpolice
- Milestone changed from 7.6.2 to 7.10.1
Moving to 7.10.1.
comment:16 Changed 9 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 Changed 4 weeks ago by goldfire
- Architecture changed from x86_64 (amd64) to Unknown/Multiple
- Differential Revisions 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 4 weeks 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 4 weeks 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.
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.