Opened 5 years ago

Closed 7 weeks 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 (28)

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

  • Milestone changed from 7.6.2 to 7.10.1

Moving to 7.10.1.

comment:16 Changed 14 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 6 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 6 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 6 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 5 months ago by thoughtpolice

  • Milestone changed from 7.12.1 to 8.0.1

Milestone renamed

comment:21 Changed 5 months ago by jstolarek

  • Cc jstolarek added; jan.stolarek@… removed

comment:22 Changed 5 months ago by WrenThornton

  • Cc wren@… added

comment:23 in reply to: ↑ 17 Changed 5 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 5 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 5 months ago by goldfire

  • Blocking 10770 added

comment:26 Changed 8 weeks ago by goldfire

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

comment:27 Changed 7 weeks 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 7 weeks 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.

Note: See TracTickets for help on using tickets.