Opened 6 months ago

Closed 6 months ago

Last modified 5 months ago

#13524 closed bug (fixed)

GHC does not preserve order of forall'd vars with TypeApplications

Reported by: crockeea Owned by:
Priority: normal Milestone: 8.2.1
Component: Compiler Version: 8.0.2
Keywords: TypeApplications Cc: niteria
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: typecheck/should_compile/T13524
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

The following code compiles with 8.0.2. Note that the order of variables on pt1 is a :: * and expr :: * -> *, and this is the order of the type application in main.

{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}

{-# OPTIONS_GHC -fno-warn-partial-type-signatures #-}

type Empty a = ()

foo :: expr a -> expr a -> expr (Empty a)
foo = undefined

newtype Expr a = SPT {run :: String}

pt1 :: forall a ptexpr . ptexpr a -> ptexpr (Empty a)
--pt1 :: forall a ptexpr . ptexpr a -> ptexpr _
pt1 a = foo a a

main :: IO ()
main = putStrLn $ run $ pt1 @Int @Expr undefined

If I use partial type signatures with the alternate signature for pt1 (which has the same order of the forall), I get these errors:

Bug.hs:19:25: error:
    • Couldn't match type ‘Int’ with ‘Expr’
      Expected type: Expr (Empty Expr)
        Actual type: Int (Empty Expr)
    • In the second argument of ‘($)’, namely
        ‘pt1 @Int @Expr undefined’
      In the second argument of ‘($)’, namely
        ‘run $ pt1 @Int @Expr undefined’
      In the expression: putStrLn $ run $ pt1 @Int @Expr undefined

Bug.hs:19:30: error:
    • Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’
    • In the type ‘Int’
      In the second argument of ‘($)’, namely ‘pt1 @Int @Expr undefined’
      In the second argument of ‘($)’, namely
        ‘run $ pt1 @Int @Expr undefined’

Bug.hs:19:35: error:
    • Expecting one more argument to ‘Expr’
      Expected a type, but ‘Expr’ has kind ‘* -> *’
    • In the type ‘Expr’
      In the second argument of ‘($)’, namely ‘pt1 @Int @Expr undefined’
      In the second argument of ‘($)’, namely
        ‘run $ pt1 @Int @Expr undefined’

The errors are saying that the kinds of the type applications are incorrect, but nothing in the order of pt1s forall nor the order of application has changed.

However, if I then change the order of the type applications in main to main = putStrLn $ run $ pt1 @Expr @Int undefined, GHC accepts the program, even though the kinds of types in the application are incorrect with respect to the order listed in pt1 (so it should reject the program).

Somehow GHC has swapped the order of a and ptexpr in the variable list for pt1.

Change History (15)

comment:1 Changed 6 months ago by RyanGlScott

Keywords: TypeApplications added

Even spookier, this actually works on GHC 8.0.1—it's only in GHC 8.0.2 (and HEAD) that I can reproduce the incorrect type variable order when using the partial type signature.

comment:2 Changed 6 months ago by RyanGlScott

Cc: niteria added

This regression first popped up in c9bcaf3165586ac214fa694e61c55eb45eb131ab (Kill varSetElemsWellScoped in quantifyTyVars). You can also reproduce the same error in GHC 8.0.1 by compiling with -dunique-increment=-1 (after uncommenting the partial type signature, of course).

cc'ing niteria, in case he has an idea of what might be happening here.

comment:3 Changed 6 months ago by niteria

Hmm, I would have expected 7e96526ac2ef5987ecb03217d3d616b6281c1441 to fix it and #13371 to be related. But you tested with HEAD, so that's a bit odd.

comment:4 Changed 6 months ago by goldfire

Hmm. When the user gives a partial type signature, a whole new code path is used when checking the function. It seems this code path does not respect the order of specified type variables. @niteria's patch likely just exposed the underlying fragility; I don't think investigating that patch will yield any tasty fruit.

I'm afraid I'm unable to address this right now, unfortunately. We could advertise this as an infelicity (I'm fairly confident the problem will happen only with a partial type signature). Perhaps even better, we could label variables in partial type signatures as "inferred", meaning that GHC will prevent them from being available for type application.

comment:5 Changed 6 months ago by simonpj

Perhaps even better, we could label variables in partial type signatures as "inferred", meaning that GHC will prevent them from being available for type application.

Yes! After all, if you write

f :: forall a. _ -> a -> a
f = ...

you might end up with more type variables; e.g. f's signature might really be

f :: forall a b c. (b,c) -> a -> a

comment:6 Changed 6 months ago by crockeea

I'm confused here: are you suggesting that you would be able to apply f to a, but not to b or c, or are you saying you would disallow type applications completely on functions that have partial type signatures?

In the former case, new variables aren't causing my issue; GHC is reordering explicitly listed variables. In the latter case, this really weakens these two features! I'd rather guess the right order through trial and (compile) error than be disallowed completely.

comment:7 Changed 6 months ago by RyanGlScott

I think there's a bit of confusion here. The issue is not that wildcards are being treated as visible type variables, as evidenced in this GHCi session:

$ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive
GHCi, version 8.3.20170329: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
λ> :set -fprint-explicit-foralls -XPartialTypeSignatures
λ> let foo :: _ -> b; foo _ = undefined

<interactive>:2:12: warning: [-Wpartial-type-signatures]
    • Found type wildcard ‘_’ standing for ‘w’
      Where: ‘w’ is a rigid type variable bound by
               the inferred type of foo :: w -> b at <interactive>:2:20-36
    • In the type signature: foo :: _ -> b
λ> :type +v foo
foo :: forall {w} b. w -> b

The fresh type variable that gets used in place of _ is implicitly quantified and unspecified, so it is not available for visible type application in the first place:

λ> :set -XTypeApplications 
λ> :type +v foo @Int
foo @Int :: forall {w}. w -> Int
λ> :type +v foo @Int @Char

<interactive>:1:1: error:
    • Cannot apply expression of type ‘w0 -> Int’
      to a visible type argument ‘Char’
    • In the expression: foo @Int @Char

This part is working as expected. The issue is the order in which the explicitly quantified type variables are being returned in the presence of PartialTypeSignatures. If you take this code

{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}

{-# OPTIONS_GHC -fno-warn-partial-type-signatures #-}

type Empty a = ()

foo :: expr a -> expr a -> expr (Empty a)
foo = undefined

newtype Expr a = SPT {run :: String}

pt1 :: forall a ptexpr . ptexpr a -> ptexpr _
pt1 a = foo a a

and load it into GHCi, you can see for yourself the exact (incorrect) order in which pt1's type variables are appearing:

$ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.3.20170329: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )
Ok, modules loaded: Main.
λ> :set -fprint-explicit-foralls 
λ> :type +v pt1
pt1 :: forall (ptexpr :: * -> *) a. ptexpr a -> ptexpr (Empty a)

comment:8 Changed 6 months ago by RyanGlScott

I heartily agree with crockeea that we should not disable VTA altogther for things with partial type signatures. I think that would be even more confusing than the current behavior, in fact!

comment:9 Changed 6 months ago by crockeea

@RyanGlScott Thank you for helping to clear up the question; you nailed it.

comment:10 Changed 6 months ago by Ben Gamari <ben@…>

In 5b7f504/ghc:

testsuite: Add test for #13524

Reviewers: austin

Subscribers: rwbarton, thomie

Differential Revision: https://phabricator.haskell.org/D3418

comment:11 Changed 6 months ago by goldfire

My comment:4 says:

Perhaps even better, we could label variables in partial type signatures as "inferred", meaning that GHC will prevent them from being available for type application.

This was always meant to be a stopgap solution, in case the status quo is unacceptable for 8.2. I've already put this bug in my queue for my summer bug roundup. But I simply can't get to it in the next month. "Even better" is suggesting that reliable, explainable behavior is better than capricious behavior, but @crockeea's comment:6 disagrees with this suggestion. I certainly don't feel strongly.

comment:12 Changed 6 months ago by Simon Peyton Jones <simonpj@…>

In 0ae72512/ghc:

Yet more work on TcSimplify.simplifyInfer

The proximate cause for this patch is Trac #13482, which pointed out
further subtle interactions between
   - Inferring the most general type of a function
   - A partial type signature for that function

That led me into /further/ changes to the shiny new stuff in
TcSimplify.simplifyInfer, decideQuantification, decideMonoTyVars,
and related functions.

Happily, I was able to make some of it quite a bit simpler,
notably the bit about promoting free tyvars.  I'm happy with
the result.

Moreover I fixed Trac #13524 at the same time.  Happy days.

comment:13 Changed 6 months ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: typecheck/should_compile/T13524

I fixed this, somewhat by accident. The key code is in TcSimplify.decideQuantifiedTyVars, where there is a comment to explain.

comment:14 Changed 6 months ago by crockeea

Will this make 8.2.1, or even 8.2 rc2?

comment:15 Changed 5 months ago by bgamari

Milestone: 8.2.1

Yes, I've merged this to ghc-8.2 as 4db9fd73cd452cf235117598ec13daae851e9cd7.

Last edited 5 months ago by bgamari (previous) (diff)
Note: See TracTickets for help on using tickets.