Implement Partial Type Signatures
ClosedPublic

Authored by thomasw on Aug 19 2014, 5:13 AM.

Details

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Lint
Automatic diff as part of commit; lint not applicable.
Unit
Automatic diff as part of commit; unit tests not applicable.
There are a very large number of changes, so older changes are hidden. Show Older Changes
simonpj added inline comments.Nov 17 2014, 9:09 AM
compiler/typecheck/TcBinds.lhs
1415

I think (1) is what is required. Logically, the type signature is being instantiated "inside" the typechecking for the RHS.

Can you give a small test case where the invariant then fails?

In D168#12289, @thomasw wrote:

Just to be sure: the syntactic diff approach you have in mind, it's not just about how to calculate the diff between the final context and the annotated context of a binding, right? (You mentioned something about getting rid of "20-40 lines of dense code")

I'm suggesting something incredibly simple.

The user supplies a signature

f :: (Ord a, _) => blah

Ignoring the user-supplied context entirely, but taking account of 'blah', we infer a type

f :: (Ix a, Ord a, C a) =>  blah

Now take that inferred context and remove the bit the user supplied. Something like

filterOut (`elem` user_supplied_ctxt) inferred_ctxt

And that is what we report for the "_". So simple! Not clever, but simple. No unification. No implications, no abs_ev_vars. Just filterOut.

Does that make sense?

Simion

In D168#12295, @simonpj wrote:
In D168#12289, @thomasw wrote:

Just to be sure: the syntactic diff approach you have in mind, it's not just about how to calculate the diff between the final context and the annotated context of a binding, right? (You mentioned something about getting rid of "20-40 lines of dense code")

I'm suggesting something incredibly simple.

The user supplies a signature

f :: (Ord a, _) => blah

Ignoring the user-supplied context entirely, but taking account of 'blah', we infer a type

f :: (Ix a, Ord a, C a) =>  blah

Now take that inferred context and remove the bit the user supplied. Something like

filterOut (`elem` user_supplied_ctxt) inferred_ctxt

And that is what we report for the "_". So simple! Not clever, but simple. No unification. No implications, no abs_ev_vars. Just filterOut.

Does that make sense?

Simion

That's indeed very simple, but what about the following example:

f :: (Ord a, Num a, _) => blah

Ignoring the user-supplied context entirely, but taking account of 'blah', we infer a type

f :: (Ix a, Ord a, C a) =>  blah

Mind that Num a is not inferred, only annotated.

filterOut (`elem` user_supplied_ctxt) inferred_ctxt

will then report (Ix a, C a) for the _ (perfectly fine) and use (Ord a, Ix a, C a) as final context. The Num a constraint has completely disappeared! This is what you intend, right? I find that very counter-intuitive, but you have the final say of course :-)

The only robust way I currently see to still let annotated constraints that are not inferred persist into the final context, is with an implication.

bandwidth too low. Skype now? I'm simonpj0

thomasw added inline comments.Nov 17 2014, 9:41 AM
compiler/typecheck/TcBinds.lhs
1415

If I replace the line above with:

(nwc_tvs, _) <- captureUntouchables $ mapM newWildcardVarMetaKind wcs

I believe it will fail for just about any partial type signature containing a wildcard, anonymous or not (except for extra-constraints wildcards, which are something totally different).

The MetaTvInv fails, as the level number of these unification variables is 2 (because of the captureUntouchables call), but the level number of the enclosing context is 1 (because apparently there is no parent Implication when the unification happens).

thomasw updated this revision to Diff 1467.Nov 17 2014, 10:51 AM
  • Make wildcard meta vars with the right level number
  • Simplify taking the annotated constraints into account
In D168#12304, @thomasw wrote:
  • Make wildcard meta vars with the right level number
  • Simplify taking the annotated constraints into account

The whole message of the second commit is:

No longer create an implication, just infer the type from scratch, add the annotated constraints that weren't inferred to theta, and use tcSubType to 'fix' things.

Unfortunately there's still a problem with the ev_binds I believe. Compile the example below with -dcore-lint. It does work when annotating just Eq a in showAndEq2's context, but not when annotating just Show a. It's a problem with the order of the arguments in Core.

{-# LANGUAGE PartialTypeSignatures #-}
module Problem1 where

showAndEq :: _ => a -> String
showAndEq x = show x ++ show (x == x)

showAndEq2 :: (Show a, _) => a -> String
showAndEq2 x = showAndEq x
thomasw updated this revision to Diff 1468.Nov 17 2014, 11:22 AM

Fix build

The build stills fails because Phabricator doesn't look at my fork of
Haddock that supports Partial Type Signatures

thomasw added inline comments.Nov 17 2014, 11:34 AM
compiler/typecheck/TcHsType.lhs
542

This line is the culprit of the MetaTvInv violation. checkExpectedKind uses unifyKindX, which uses uKVar, which calls lookupTcTyVar, which checks whether the kind variable is touchable using isTouchableTcM, which uses isTouchableMetaTyVar, which checks the invariant in an assert, which fails.

As this is done during type-checking the signature, and not the body, the level number of the context is indeed not increased.

The solution I propose is to wrap this line in a call to captureConstraints. This should be safe, as this case only deals with wildcards which were already created in the scope of an extra call to captureConstraints.

simonpj added inline comments.Nov 17 2014, 3:49 PM
compiler/typecheck/TcHsType.lhs
542

As I said in email, please don't mess with tc_hs_type. Rather put the call to tcHsSigType in tcTySig under the same captureUntouchables as the newWildCardMetaVars calls.

If you post status/new patch/update I'll look tomorrow.

Simon

thomasw updated this revision to Diff 1486.Nov 18 2014, 3:29 AM
  • Properly maintain the MetaTvInv invariant

Your tip to use tcSubType to take care of the annotated but not inferred constraints simplifies things greatly. Unfortunately, there is still something wrong.

Take the following simple program:

foo :: (Num a, _) => a -> String
foo x = show x

Num a is annotated, but not inferred. This type-checks and the correct type for foo is inferred (forall a. (Num a, Show a) => a -> String). However, when enabling the -dcore-lint flag, the following error is found:

In the expression:
  (\ (@ a_avf) ($dShow_aEC :: Show a_avf) ->
  let { $dShow_avp :: Show a_avf
        $dShow_avp = $dShow_aEC }
  in letrec { foo_avg :: a_avf -> String
              foo_avg = \ (x_amy :: a_avf) -> show @ a_avf $dShow_avp x_amy }
     in foo_avg)
  @ a_aEE $dNum_aEJ $dShow_aEK
    Argument value doesn't match argument type:
    Fun type: Show a_aEE => a_aEE -> String
    Arg type: Num a_aEE
    Arg: $dNum_aEJ

The whole Core program (I've removed some annotations).

foo :: forall a_avf. (Num a_avf, Show a_avf) => a_avf -> String
foo = \ (@ a_aEE) ($dNum_aEF :: Num a_aEE) ($dShow_aEG :: Show a_aEE) ->
    let { $dShow_aEK :: Show a_aEE
          $dShow_aEK = $dShow_aEG }
    in let { $dNum_aEJ :: Num a_aEE
             $dNum_aEJ = $dNum_aEF }
       in (\ (@ a_avf) ($dShow_aEC :: Show a_avf) ->
          let { $dShow_avp :: Show a_avf
                $dShow_avp = $dShow_aEC }
          in letrec { foo_avg :: a_avf -> String
                      foo_avg = \ (x_amy :: a_avf) -> show @ a_avf $dShow_avp x_amy }
             in foo_avg)
          @ a_aEE $dNum_aEJ $dShow_aEK

The error tells us that a Num a* dictionary is passed when a Show a* dictionary is expected. The problem is that the lambda the error starts with doesn't accept a Num a* dictionary as second argument (after the type argument and before the Show a* dictionary).

I think it has something to do with the abs_ev_vars of the AbsBinds created in tcPolyInfer not being updated.

simonpj added inline comments.Nov 18 2014, 7:43 AM
compiler/typecheck/TcBinds.lhs
567

If we are doing PolyCheck, surely there are no wildards? So assert null nwcs?

If I'm wrong, add a comment to say so.

612

What's all this tyvar-env extension stuff? It's not present in the baseline compiler. Why is it needed here?

thomasw added inline comments.Nov 18 2014, 8:23 AM
compiler/typecheck/TcBinds.lhs
567

You're right. This is a leftover from some early experimentation.
I'll add an assert and fix line 572.

612

We have to bring the type variables and named wildcards into scope here for nested bindings, e.g.

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PartialTypeSignatures #-}
-- The '_' is required to get into tcPolyInfer
f :: forall a. a -> (a, _)
f x = g False
  where
    -- without L607, this 'a' would be out of scope.
    g :: forall t. t -> (a, String)
    g _ = (x, "")

The example above is for type variables, but can be changed to named wildcards.

Notes above.Did you get my patch (sent by email)?

compiler/typecheck/TcBinds.lhs
612

Ah... I see. The new feature is that previously in any situation where scoped type variables applied, we'd be in tcPolyCheck.

But it's wrong as-is. In a mutually recursive group, you are making ALL the forall'd varaibles scope over ALL the bindings.

Instead we should drop the tcExtendTyVarEnv2 from tcPolyCheck and tcPolyInfer, and instead do it in the FunBind case of tcRhs. That'll catch all the cases in one place. Make sense?

Simon

thomasw updated this revision to Diff 1496.Nov 18 2014, 8:47 AM
  • There can't be wildcards if we're in tcPolyCheck
thomasw added inline comments.Nov 18 2014, 8:57 AM
compiler/typecheck/TcBinds.lhs
612

Ok, makes sense, the concat felt ugly from the start.

I haven't received your email yet, some other people here (@cs.kuleuven.be) have also noticed that emails from @microsoft.com take a long time to arrive.

I'll look at your patch as soon as I get it. Does your patch move tcExtendTyVarEnv2 to tcRhs?

612

This concat feels ugly too.

Bother. Why doesn't email work? Anyway

Apply the attached patch, and all should be well.

As a separate patch I think HsForAllTy should be a record with named fields, if you felt like doing that.

At the moment if you *don't* say PartialTypeSignatures you get informative error messages. If you *do*, all the messages go away. Shouldn’t they turn into warnings?

Simon

PS: no it doesn't implement the tcRhs stuff. It deals with the extra constraints thing you were struggling with.

In D168#12558, @simonpj wrote:

Bother. Why doesn't email work? Anyway

Something about a Greylist, I have asked sysadmins to look into it.

Apply the attached patch, and all should be well.

Applied, I'll upload here in a second.

As a separate patch I think HsForAllTy should be a record with named fields, if you felt like doing that.

At the moment if you *don't* say PartialTypeSignatures you get informative error messages. If you *do*, all the messages go away. Shouldn’t they turn into warnings?

That was my initial goal as well, but after changing to the insoluble constraint approach, it became quite a bit harder to do so.

thomasw updated this revision to Diff 1499.Nov 18 2014, 9:26 AM
  • Apply Simon's patch
thomasw updated this revision to Diff 1500.Nov 18 2014, 9:45 AM
  • Move the call to tcExtendTyVarEnv2 into tcRhs

At the moment if you *don't* say PartialTypeSignatures you get informative error messages. If you *do*, all the messages go away. Shouldn’t they turn into warnings?

That was my initial goal as well, but after changing to the insoluble constraint approach, it became quite a bit harder to do so.

Would you care to elaborate on what was difficult?

In D168#12590, @simonpj wrote:

At the moment if you *don't* say PartialTypeSignatures you get informative error messages. If you *do*, all the messages go away. Shouldn’t they turn into warnings?

That was my initial goal as well, but after changing to the insoluble constraint approach, it became quite a bit harder to do so.

Would you care to elaborate on what was difficult?

For the extra-constraints wildcard/hole, it's easy, but for regular wildcards it's different. By default, I emit insoluble constraints for each wildcard, which are leftover after solving the constraints and are then converted into error messages. In the case that -XPartialTypeSignatures is on, I don't emit insoluble constraints as I want constraint solving to succeed, so after solving the constraints I have nothing to make errors of. I didn't find a clean way to have access to these wildcards after the constraint solver is done (including the module-wide simplifyTop in tcRnSrcDecls on line 473 in TcRnDriver).

I believe it would be incorrect to report warnings in mkExport, as defaulting hasn't taken place yet.

P.S. I still haven't received your email, but posting patches here works well.

thomasw updated this revision to Diff 1501.Nov 18 2014, 10:21 AM

Fix case of no extra-constraints wildcards

When there is no extra-constraints wildcard, completeTheta should return the
annotated constraints as final theta instead of the inferred, e.g.

foo :: Num a => a -> _
foo x = x

We should return (Num a), not [], as without an extra-constraints wildcard, no
extra constraints can be inferred, so inferred_theta must be empty anyway.

simonpj added inline comments.Nov 18 2014, 10:29 AM
compiler/typecheck/TcBinds.lhs
762

Why do you think inferred_theta is empty?

Would you care to elaborate on what was difficult?

For the extra-constraints wildcard/hole, it's easy, but for regular wildcards it's different. By default, I emit insoluble constraints for each wildcard, which are leftover after solving the constraints and are then converted into error messages. In the case that -XPartialTypeSignatures is on, I don't emit insoluble constraints as I want constraint solving to succeed, so after solving the constraints I have nothing to make errors of. I didn't find a clean way to have access to these wildcards after the constraint solver is done (including the module-wide simplifyTop in tcRnSrcDecls on line 473 in TcRnDriver).

I don't see the problem. Just emit the constraints anyway! For TypedHoles we do that, and the TcErrors processing turns them into warnings.

Simon

thomasw added inline comments.Nov 18 2014, 10:33 AM
compiler/typecheck/TcBinds.lhs
762

The function completeTheta is only called when we're dealing with a partial type signature. Only when an extra-constraints wildcard was present, i.e. the Just loc <- mb_extra_cts case, were we allowed to infer extra constraints. So in this case, no extra constraints were allowed to be inferred, so inferred_theta must be empty.

simonpj added inline comments.Nov 18 2014, 10:40 AM
compiler/typecheck/TcBinds.lhs
762

I don't agree (or I am misunderstanding). Consider

f :: forall a. Eq a => _ -> a -> Int
f True x = if x==x then 1 else 2

This is a partial signature. There is no extra-constraint wildard. But the inferred theta includes Eq a.

In D168#12598, @simonpj wrote:

Would you care to elaborate on what was difficult?

For the extra-constraints wildcard/hole, it's easy, but for regular wildcards it's different. By default, I emit insoluble constraints for each wildcard, which are leftover after solving the constraints and are then converted into error messages. In the case that -XPartialTypeSignatures is on, I don't emit insoluble constraints as I want constraint solving to succeed, so after solving the constraints I have nothing to make errors of. I didn't find a clean way to have access to these wildcards after the constraint solver is done (including the module-wide simplifyTop in tcRnSrcDecls on line 473 in TcRnDriver).

I don't see the problem. Just emit the constraints anyway! For TypedHoles we do that, and the TcErrors processing turns them into warnings.

Ok, for TypedHoles, you turn them into warnings when -fdefer-type-errors is on. So we have to do something similar when PartialTypeSignatures is on, but only for CHoleCan constraints generated by holes in a type signature. Maybe change maybeReportError or add a separate reporter for holes in a signature?

In D168#12608, @thomasw wrote:
In D168#12598, @simonpj wrote:

Would you care to elaborate on what was difficult?

For the extra-constraints wildcard/hole, it's easy, but for regular wildcards it's different. By default, I emit insoluble constraints for each wildcard, which are leftover after solving the constraints and are then converted into error messages. In the case that -XPartialTypeSignatures is on, I don't emit insoluble constraints as I want constraint solving to succeed, so after solving the constraints I have nothing to make errors of. I didn't find a clean way to have access to these wildcards after the constraint solver is done (including the module-wide simplifyTop in tcRnSrcDecls on line 473 in TcRnDriver).

I don't see the problem. Just emit the constraints anyway! For TypedHoles we do that, and the TcErrors processing turns them into warnings.

Ok, for TypedHoles, you turn them into warnings when -fdefer-type-errors is on. So we have to do something similar when PartialTypeSignatures is on, but only for CHoleCan constraints generated by holes in a type signature. Maybe change maybeReportError or add a separate reporter for holes in a signature?

So are you saying that you need to distinguish CHoleCan constraints, so that you can tell which come from partial type sigs, and which from holes in expressions? That doesn't sound too hard! Go for it.

thomasw added inline comments.Nov 18 2014, 10:56 AM
compiler/typecheck/TcBinds.lhs
762

Indeed it should include Eq a, but so will annotated_theta.
The assert is incorrect, but I do think we should return annotated_theta in this case (this matters when there is a constraint annotated which is not inferred).

These examples actually don't work with this version of the code, nor with the one you sent me in the patch :(

I get:

No instance for (Eq a)
  arising from the inferred type of f :: Eq a => _ -> a -> Int

I'll look into it tomorrow.

In D168#12610, @simonpj wrote:
In D168#12608, @thomasw wrote:
In D168#12598, @simonpj wrote:

Would you care to elaborate on what was difficult?

For the extra-constraints wildcard/hole, it's easy, but for regular wildcards it's different. By default, I emit insoluble constraints for each wildcard, which are leftover after solving the constraints and are then converted into error messages. In the case that -XPartialTypeSignatures is on, I don't emit insoluble constraints as I want constraint solving to succeed, so after solving the constraints I have nothing to make errors of. I didn't find a clean way to have access to these wildcards after the constraint solver is done (including the module-wide simplifyTop in tcRnSrcDecls on line 473 in TcRnDriver).

I don't see the problem. Just emit the constraints anyway! For TypedHoles we do that, and the TcErrors processing turns them into warnings.

Ok, for TypedHoles, you turn them into warnings when -fdefer-type-errors is on. So we have to do something similar when PartialTypeSignatures is on, but only for CHoleCan constraints generated by holes in a type signature. Maybe change maybeReportError or add a separate reporter for holes in a signature?

So are you saying that you need to distinguish CHoleCan constraints, so that you can tell which come from partial type sigs, and which from holes in expressions? That doesn't sound too hard! Go for it.

Ok, I guess a flag check in mkHoleError and a call to makeIntoWarning will do it. I'll do it tomorrow.

simonpj added inline comments.Nov 18 2014, 11:14 AM
compiler/typecheck/TcBinds.lhs
762

OK, so inferred-theta and annotated-theta both contain Eq a. Very good. So we are agreed that the assert (null inferred-theta) is indeed wrong.

I'm not sure about the type error. Let me know if you get stuck

thomasw updated this revision to Diff 1541.Nov 19 2014, 3:54 AM
  • Remove wrong ASSERT.
  • Fix: constraints were forgotten when there was no extra-constraints wildcard

    The Eq a constraint in the example below was forgotten:

    f :: Eq a => _ -> a -> Int f True x = if x == x then 1 else 2

    Remove obsolete code and minimise the diff at the same time. Also update changed error messages.
thomasw updated this revision to Diff 1548.Nov 19 2014, 6:53 AM
  • Report wildcard instantiations as warnings when -XPartialTypeSignatures is on
thomasw updated this revision to Diff 1549.Nov 19 2014, 8:34 AM
  • Better error context for wildcards in expression signatures
  • Update some tests
thomasw updated this revision to Diff 1630.Nov 21 2014, 10:19 AM

Refactor against lastest master

thomasw updated this revision to Diff 1634.Nov 21 2014, 11:24 AM
  • Remove isWildcardCt
  • Mark failing tests as bugs
thomasw updated this revision to Diff 1647.Nov 21 2014, 2:48 PM

Rebase against master, i.e. the API annotations

thomasw updated this revision to Diff 1702.Nov 24 2014, 4:11 AM

Rebase against master

thomasw added inline comments.Nov 24 2014, 5:06 AM
compiler/typecheck/TcErrors.lhs
178

I'd like to add a similar flag that will control whether warnings for holes in (partial) type signatures should be suppressed or not. Any ideas for a good name?

Some ideas:

  • -fwarn-partial-type-signatures
  • -fwarn-holes-in-types
  • ...

I'm gonna go ahead and try to implement this (it should quite easy), the flag can always be renamed later.

thomasw updated this revision to Diff 1707.Nov 24 2014, 10:22 AM
  • Add -fwarn-holes-in-types
  • Update the manual
simonpj accepted this revision.Nov 24 2014, 11:31 AM
simonpj edited edge metadata.

I see you have added the user manual documentation, thanks.

Are you ready to merge? Your ToDo list is not empty, but I think we should merge,if you feel ready. I hope you'll keep working on the to-do list.

Simon

compiler/typecheck/TcErrors.lhs
178

-fwarn-partial-type-signatures, since that is the name of the language extension.

I've told Austin that I'm ready to merge. I hope to tackle the rest of
my TODOs as soon as I can. A little help would be welcome.

As you've accepted my revision I don't think I'm still able to change
the name of the flag to -fwarn-partial-type-signatures, but that can be
fixed after the merge (or during).

@thomasw You can always run arc diff again to update something, even once it's been accepted. Either way, I'll just land this - you can submit another patch to fix the flag name afterwords. :)

thomasw updated this revision to Diff 1716.Nov 25 2014, 2:48 AM
thomasw edited edge metadata.
  • Rename -fwarn-holes-in-types to -fwarn-partial-type-signatures
thomasw updated this revision to Diff 1717.EditedNov 25 2014, 4:04 AM

Update my e-mail address in the first commit

thomasw updated this revision to Diff 1735.Nov 26 2014, 5:06 AM
  • Disallow wildcards in pattern synonym type signatures
This revision was automatically updated to reflect the committed changes.
hvr added a subscriber: hvr.Nov 29 2014, 6:19 AM

Landing this has resulted in several validate failures such e.g.

Actual stderr output differs from expected:
--- ./indexed-types/should_fail/SimpleFail5b.stderr	2014-03-01 00:16:55.447540890 +0100
+++ ./indexed-types/should_fail/SimpleFail5b.comp.stderr	2014-11-29 13:15:14.330002603 +0100
@@ -1,4 +1,9 @@
 
+SimpleFail5b.hs:30:21:
+    No instance for (Num Char) arising from the literal ‘1’
+    In the expression: 1
+    In an equation for ‘bar3wrong'’: bar3wrong' D3Int = 1
+
 SimpleFail5b.hs:31:12:
     Couldn't match type ‘Char’ with ‘Int’
     Expected type: S3 Int
*** unexpected failure for SimpleFail5b(normal)

...were these changes in compiler errors really expected?

In D168#14532, @hvr wrote:

Landing this has resulted in several validate failures such e.g.

Actual stderr output differs from expected:
--- ./indexed-types/should_fail/SimpleFail5b.stderr	2014-03-01 00:16:55.447540890 +0100
+++ ./indexed-types/should_fail/SimpleFail5b.comp.stderr	2014-11-29 13:15:14.330002603 +0100
@@ -1,4 +1,9 @@
 
+SimpleFail5b.hs:30:21:
+    No instance for (Num Char) arising from the literal ‘1’
+    In the expression: 1
+    In an equation for ‘bar3wrong'’: bar3wrong' D3Int = 1
+
 SimpleFail5b.hs:31:12:
     Couldn't match type ‘Char’ with ‘Int’
     Expected type: S3 Int
*** unexpected failure for SimpleFail5b(normal)

...were these changes in compiler errors really expected?

My apologies, the failures are caused by a recent incorrect refactoring of mine. I've attached a patch that fixes all the failures Edward mentioned in the mailing list, including the one you mention.

On 29-11-14 06:16, Edward Z. Yang wrote:

I get these fails:

TEST="overloadedlistsfail03 overloadedlistsfail05 sigof02dt sigof02dmt annfail07 FD3 T5689 T7696 T5978 FDsFromGivens tcfail178 tcfail014 T8603 tcfail143 tcfail200 T9612 tcfail159 T7368 T5570 T6069 T5691 T7368a T8262 T7851 T8392a T5246 tcfail123 tcfail122 tcfail090 mc24 mc25 mc22 mc23 T3950 tcfail165 T8142 T5462Yes1 T5462Yes2 T3169 SimpleFail5b T3330c T5439 T7729 T7354a T7354 T7729a T7786"

Mostly stderr changes.

hvr added a comment.Nov 29 2014, 10:08 AM
In D168#14547, @thomasw wrote:

My apologies, the failures are caused by a recent incorrect refactoring of mine. I've attached a patch that fixes all the failures Edward mentioned in the mailing list, including the one you mention.

Could you please create a differential from that patch?