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

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 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:

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

Note: See TracTickets for help on using tickets.