GHC 9.0 no longer typechecks a program involving overloaded labels and type applications

In the program that follows, I specify the type of a label by using a visible type application.

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE OverloadedLabels       #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE RebindableSyntax       #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeApplications       #-}

module Labels where

-- base
import Prelude
import Data.Kind
  ( Type )
import GHC.TypeLits
  ( Symbol, KnownSymbol )

--------------------------------------------------------------------------

data Label (k :: Symbol) (a :: Type) = Label

class IsLabel k a v | v -> a, v -> k where
  fromLabel :: v

instance KnownSymbol k => IsLabel k a (Label k a) where
  fromLabel = Label @k @a

foo :: Label k a -> ()
foo _ = ()

test :: ()
test = foo ( #label @Bool )

The point of this program is that the label #label is polymorphic:

#label :: forall (a :: Type). Label "label" a

and I am able to instantiate the type variable a with a type application.

Show/hide further context.

This was boiled down from the overloaded label syntax I provide in my shader library, see here.

This added bit of syntax allows users of the library to write shaders in an imperative style, see here for an example.

This program compiles fine on GHC 8.10 (and previous GHC versions), but fails to compile on GHC 9.0 (rc1) with the following error:

Labels.hs:35:14: error:
    * Cannot apply expression of type `v0'
      to a visible type argument `Bool'
    * In the first argument of `foo', namely `(#label @Bool)'
      In the expression: foo (#label @Bool)
      In an equation for `test': test = foo (#label @Bool)
   |
35 | test = foo ( #label @Bool )
   |              ^^^^^

Can someone enlighten me about what's going on? I found it quite useful to be able to pass further arguments to an overloaded label in this way, whereas I now have to write something like

test :: ()
test = foo ( #label :: Label _ Bool )

to specify a, which defeats the purpose of the overloaded labels syntax. At that point I might as well just write:

foo ( Label @"label" @Bool )

added Tbug program incorrectly rejected typechecker labels

changed the description

changed the description

Ah, I assume this must be a consequence of eager instantiation. So the following works:

test :: ()
test = foo ( ( #label :: forall a. Label "label" a ) @Bool )

Is there any way to recover the more concise syntax? I was using it to allow users to write imperative-style code such as:

loop = do
  #i @Word32 #= 0
  while ( #i < 10 ) do
    #i %= (+1)
  #i

which desugars to

loop = do
  _ <- def @"i" @RW @Word32 0
  while ( get @"i" < 10 ) do
    modify @"i" (+1)
  get @"i"

so it's kind of unfortunate that this trick no longer works (but not critically important either).

changed the description

This is my fault when implementing Quick Look. Should not be hard to fix.

Actually your example was more subtle than I originally realised. In your case

fromLabel :: forall {k1} {k2}. forall (a::k1). blah

So GHC has to instantiate those inferred quantifiers k1 and k2 before it comes to (a:k1) which it must instantiate with "label"::Symbol.

All this should be done as part of inferring the type of a "head" (see Note [Application chains and heads] in GHC.Tc.Gen.App.).

Patch incoming.

mentioned in merge request !4722 (closed)

This is my fault when implementing Quick Look. Should not be hard to fix.

I'm a bit confused by this comment. This is a regression that occurs in 9.0, which lacks Quick Look. How, then, could Quick Look be responsible for this regression?

mentioned in commit f1c4b2e3

I'm a bit confused by this comment. This is a regression that occurs in 9.0, which lacks Quick Look.

Ah yes. I think the offending commit is actually this one, which is in 9.0.

commit ffde234854f49dba9ec4735aad74b30fd2deee29
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Wed Apr 8 23:08:12 2020 +0100

    Do eager instantation in terms
    
    This patch implements eager instantiation, a small but critical change
    to the type inference engine, #17173.  The main change is this:

Anyway it's fixed in HEAD. I suppose we could back-port to 9.0, but I wonder if @trac-sheaf will be content to wait for 9.2?

Thanks Simon, that's great.

I'm happy to wait for 9.2; I'll just add a little disclaimer in my library about the inconsistency with 9.0.

mentioned in commit aa3dd11c

mentioned in commit 4ca7c1a8

changed milestone to %9.2.1

mentioned in issue #17582

mentioned in commit 3e20ec0b

mentioned in commit a3d56282

mentioned in commit eb13c963