Opened 5 years ago

Closed 5 months ago

Last modified 3 months ago

#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

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.

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 23 months ago by thoughtpolice

  • Milestone changed from 7.6.2 to 7.10.1

Moving to 7.10.1.

comment:16 Changed 17 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: Changed 10 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:

  1. 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.
  1. 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: Changed 10 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 10 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 9 months ago by thoughtpolice

  • Milestone changed from 7.12.1 to 8.0.1

Milestone renamed

comment:21 Changed 9 months ago by jstolarek

  • Cc jstolarek added; jan.stolarek@… removed

comment:22 Changed 8 months ago by WrenThornton

  • Cc wren@… added

comment:23 in reply to: ↑ 17 Changed 8 months ago by WrenThornton

Replying to goldfire:

I have two open design questions:

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

  1. 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 8 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 8 months ago by goldfire

  • Blocking 10770 added

comment:26 Changed 5 months ago by goldfire

  • Differential Rev(s) changed from Phab:D1138 to Phab:D1681

comment:27 Changed 5 months ago by Richard Eisenberg <eir@…>

In 2db18b81/ghc:

Visible type application

This re-working of the typechecker algorithm is based on
the paper "Visible type application", by Richard Eisenberg,
Stephanie Weirich, and Hamidhasan Ahmed, to be published at
ESOP'16.

This patch introduces -XTypeApplications, which allows users
to say, for example `id @Int`, which has type `Int -> Int`. See
the changes to the user manual for details.

This patch addresses tickets #10619, #5296, #10589.

comment:28 Changed 5 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 3 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.

Last edited 3 months ago by andrewthad (previous) (diff)

comment:30 Changed 3 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.

Note: See TracTickets for help on using tickets.