Opened 3 weeks ago

Closed 12 days ago

#15330 closed bug (fixed)

Error message prints invisible kind arguments in a visible matter

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.8.1
Component: Compiler (Type checker) Version: 8.4.3
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Poor/confusing error message Test Case: typecheck/should_fail/T15330
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D4938
Wiki Page:

Description

Consider the following program:

{-# LANGUAGE RankNTypes #-}                                                                                                                                                                               
{-# LANGUAGE TypeInType #-}                                                                                                                                                                               
module Bug where                                                                                                                                                                                          
                                                                                                                                                                                                          
import Data.Kind                                                                                                                                                                                          
import Data.Proxy                                                                                                                                                                                         
                                                                                                                                                                                                          
data T :: forall a. a -> Type                                                                                                                                                                             
                                                                                                                                                                                                          
f1 :: Proxy (T True)
f1 = "foo"

f2 :: forall (t :: forall a. a -> Type).
      Proxy (t True)
f2 = "foo"

This program doesn't typecheck (for good reason). The error messages, however, are a bit iffy:

$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:11:6: error:
    • Couldn't match expected type ‘Proxy (T 'True)’
                  with actual type ‘[Char]’
    • In the expression: "foo"
      In an equation for ‘f1’: f1 = "foo"
   |
11 | f1 = "foo"
   |      ^^^^^

Bug.hs:15:6: error:
    • Couldn't match expected type ‘Proxy (t Bool 'True)’
                  with actual type ‘[Char]’
    • In the expression: "foo"
      In an equation for ‘f2’: f2 = "foo"
    • Relevant bindings include
        f2 :: Proxy (t Bool 'True) (bound at Bug.hs:15:1)
   |
15 | f2 = "foo"
   |      ^^^^^

Note that in the error message for f1, the type T 'True is printed correctly—the invisible Bool argument is omitted. However, in the error message for f2, this is not the case, as the type t Bool 'True is printed. That Bool is an invisible argument as well, and should not be printed without the use of, say, -fprint-explicit-kinds.

Change History (8)

comment:1 Changed 3 weeks ago by RyanGlScott

Unlike its cousin #15308, this ticket looks quite tricky to fix. The difference between pretty-printing the types of f1 and f2 is essentially the difference between pretty-printing TyConApp and AppTy.

With TyConApp, we have convenient access to the kind of the underlying type constructor, which makes it simple to tell which of its arguments are visible or not. As an example, when we convert a Type to an IfaceType in toIfaceTypeX, we use this tycon kind information to convert the arguments of the tycon to IfaceTcArgs. Then, when pretty-printing a Type, we first convert to an IfaceType, and then determining which arguments of an IfaceTyConApp to print is a simple matter of checking for ITC_Vis or ITC_Invis.

Things are tricker with AppTy. The type being applied in AppTy does not have its kind cached a priori, so in order to pretty-print AppTy analogously to how we pretty-print TyConApp, it seems like we'd have to:

  1. Use typeKind to get the kind of the type being applied
  2. Gather all of the arguments to the type (à la collectArgs for Exprs)
  3. Tag which arguments are invisible (à la IfaceTcArgs)

This sounds mighty gruesome, but I can't think of a simpler solution at the moment. Thoughts?

comment:2 Changed 3 weeks ago by goldfire

How about this:

data Type = ...
          | AppTy AppTyMode Type Type
          | ...

data AppTyMode
  = VanillaATM
  | InvisATM
  -- | VisDepATM   -- for visible dependent application, which will be available outside
                   -- TyConApps with https://github.com/ghc-proposals/ghc-proposals/pull/81

Every AppTy then gets tagged, at creation. IfaceAppTy naturally would get the same tags. I think AppTys aren't all that common, so the extra word shouldn't be so bad.

comment:3 Changed 3 weeks ago by RyanGlScott

That sounds good to me. Two remaining questions:

  • How should we print InvisATM-tagged types when -fprint-explicit-kinds is enabled? Using the above example, should it be f Bool 'True or f @Bool 'True? Should -dsuppress-type-applications enter the picture somewhere?
  • Would we need to pretty-print VisDepATM-tagged types differently from VanillaATM-tagged ones? That is, why should we distinguish VisDepATM at all?

comment:4 Changed 3 weeks ago by goldfire

Let's not debate VisDepATM now. That's something I've pondered for a while, but I think it matters in coercions more than types. You're right that it won't affect printing.

I quite like putting the @ on kinds with -fprint-explicit-kinds. Regardless of anything else, we should absolutely do this. I wouldn't have it interact with -dsuppress-type-applications.

comment:5 Changed 3 weeks ago by simonpj

Let's not do this in Type, but rather in IfaceType. For Type it is simply redundant info that we'll have to carry around and maintain. We only need it for pretty-printing.

IfaceType (now a slight misnomer) is intended for serialisation, either to the user or to a binary file, so adding extra info makes sense.

In practice, we are going to gather up all the args of a chain of AppTys before pretty-printing, so we can lay them out nicely. So maybe we should use

  | IfaceAppTy     IfaceType IfaceTcArgs

and then rename IfaceTcArgs to IfaceAppArgs.

comment:6 Changed 3 weeks ago by RyanGlScott

Differential Rev(s): Phab:D4938
Status: newpatch

I quite like Simon's suggestion of reusing IfaceTcArgs (renaming it to IfaceAppArgs), so I implemented just that in Phab:D4938. In particular, I decided not to mess with any of this @ or VisDep stuff for now—we can leave that for a future patch.

Last edited 3 weeks ago by RyanGlScott (previous) (diff)

comment:7 Changed 12 days ago by Ryan Scott <ryan.gl.scott@…>

In 1c353623/ghc:

Use IfaceAppArgs to store an IfaceAppTy's arguments

Summary:
Currently, an `IfaceAppTy` has no way to tell whether its
argument is visible or not, so it simply treats all arguments as
visible, leading to #15330. We already have a solution for this
problem in the form of the `IfaceTcArgs` data structure, used by
`IfaceTyConApp` to represent the arguments to a type constructor.
Therefore, it makes sense to reuse this machinery for `IfaceAppTy`,
so this patch does just that.

This patch:

1. Renames `IfaceTcArgs` to `IfaceAppArgs` to reflect its more
   general purpose.
2. Changes the second field of `IfaceAppTy` from `IfaceType` to
   `IfaceAppArgs`, and propagates the necessary changes through. In
   particular, pretty-printing an `IfaceAppTy` now goes through the
   `IfaceAppArgs` pretty-printer, which correctly displays arguments
   as visible or not for free, fixing #15330.
3. Changes `toIfaceTypeX` and related functions so that when
   converting an `AppTy` to an `IfaceAppTy`, it flattens as many
   argument `AppTy`s as possible, and then converts those arguments
   into an `IfaceAppArgs` list, using the kind of the function
   `Type` as a guide. (Doing so minimizes the number of times we need
   to call `typeKind`, which is more expensive that finding the kind
   of a `TyCon`.)

Test Plan: make test TEST=T15330

Reviewers: goldfire, simonpj, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #15330

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

comment:8 Changed 12 days ago by RyanGlScott

Resolution: fixed
Status: patchclosed
Test Case: typecheck/should_fail/T15330

This change is just invasive enough that it's probably wise not to merge this into 8.6.

Note: See TracTickets for help on using tickets.