Opened 2 years ago

Closed 2 years ago

Last modified 2 years ago

#14265 closed feature request (fixed)

kinded holes

Reported by: lspitzner Owned by:
Priority: normal Milestone: 8.4.1
Component: Compiler (Type checker) Version: 8.2.1
Keywords: PartialTypeSignatures Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: polykinds/T14265
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

For value-level holes, ghc kindly mentions the expected type. It does not do the same for holes in type signatures: mentioning the expected kind.

Change History (6)

comment:1 Changed 2 years ago by RyanGlScott

Component: CompilerCompiler (Type checker)
Keywords: PartialTypeSignatures added

You didn't give a concrete example of what you'd like to see, so I'm forced to guess. My shot-in-the-dark attempt is this program:

{-# LANGUAGE PolyKinds #-}

f :: proxy _ -> ()
f _ = ()
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:3:12: error:
    • Found type wildcard ‘_’ standing for ‘w’
      Where: ‘w’ is a rigid type variable bound by
               the inferred type of f :: proxy w -> () at Bug.hs:4:1-8
             ‘k’ is a rigid type variable bound by
               the inferred type of f :: proxy w -> () at Bug.hs:4:1-8
      To use the inferred type, enable PartialTypeSignatures
    • In the type signature: f :: proxy _ -> ()
  |
3 | f :: proxy _ -> ()
  |            ^

This output is indeed pretty skeevy-looking¸ since it points out a kind variable k in a Where: clause, but k isn't used anywhere else! Perhaps you wanted to see something like this instead?

    • Found type wildcard ‘_’ standing for ‘w’ (of kind ‘k’)
      Where: ...

comment:2 Changed 2 years ago by lspitzner

That is exactly what I meant. Polykinded was not even in my mind; it would not hurt to have the same in simpler (non-polykind) cases too, like

foo :: StateT _ _ (); foo = undefined

could produce

<interactive>:7:15: error:
    • Found type wildcard ‘_’ standing for ‘w’ (of kind ‘*’)
      Where: ‘w’ is a rigid type variable bound by
               the inferred type of foo :: StateT w w1 () at <interactive>:7:23-37
      To use the inferred type, enable PartialTypeSignatures
    • In the type signature: foo :: StateT _ _ ()

<interactive>:7:17: error:
    • Found type wildcard ‘_’ standing for ‘w1’ (of kind ‘* -> *’)
…

comment:3 Changed 2 years ago by Simon Peyton Jones <simonpj@…>

In 1b476ab5/ghc:

Improve type-error reporting

This patch does two things:

* When reporting a hole, we now include its kind if the
  kind is not just '*'.  This addresses Trac #14265

* When reporting things like "'a' is a rigid type varaible
  bound by ...", this patch arranges to group the type variables
  together, so we don't repeat the "bound by..." stuff endlessly

comment:4 Changed 2 years ago by bgamari

Milestone: 8.4.1
Resolution: fixed
Status: newclosed

comment:5 Changed 2 years ago by lspitzner

thanks!

comment:6 Changed 2 years ago by simonpj

Test Case: polykinds/T14265
Note: See TracTickets for help on using tickets.