Opened 11 months ago

Closed 9 months ago

Last modified 8 months ago

#15795 closed bug (fixed)

Core lint error with unused kind variable in data type return kind

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.6.1
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: tests/polykinds/T15795, T15795a
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Finally managed to trigger a core lint error with #12045

{-# Language    RankNTypes       #-}
{-# Language    TypeApplications #-}
{-# Language    DataKinds        #-}
{-# Language    PolyKinds        #-}
{-# Language    TypeOperators    #-}
{-# Language    GADTs            #-}
{-# Options_GHC -dcore-lint      #-}

import Data.Kind

type Cat ob = ob -> ob -> Type

data (×) :: forall (cat1 :: Cat ob1) (cat2 :: Cat ob2). Cat (ob1, ob2) where
  Prod
    :: forall
         ob1  ob2
         cat1 cat2
         a1   b1
         a2   b2 u.
       cat1 a1 b1
    -> cat2 a2 b2
    -> (×) @u '(a1, a2) '(b1, b2)

log attached from running ghci -ignore-dot-ghci <file>.hs

Attachments (1)

log (23.6 KB) - added by Iceland_jack 11 months ago.

Download all attachments as: .zip

Change History (10)

Changed 11 months ago by Iceland_jack

Attachment: log added

comment:1 Changed 9 months ago by goldfire

Cc: mnguyen removed
Keywords: TypeInType added; TypeApplications removed

This has nothing to do with visible kind application. This fails the same way:

data (×) :: forall (cat1 :: Cat ob1) (cat2 :: Cat ob2). Cat (ob1, ob2) where
  Prod
    :: forall
         ob1  ob2
         cat1 cat2
         a1   b1
         a2   b2 u.
       cat1 a1 b1
    -> cat2 a2 b2
    -> (×) '((a1 :: u), a2) '(b1, b2)

comment:2 Changed 9 months ago by monoidal

Smaller version:

{-# Language    RankNTypes       #-}
{-# Language    PolyKinds        #-}
{-# Language    GADTs            #-}
{-# Options_GHC -dcore-lint      #-}

module DF where
import Data.Kind

data F :: forall (cat1 :: ob1). ob1 -> Type where
  Prod :: F (a :: u)

comment:3 Changed 9 months ago by RyanGlScott

Summary: Core lint error with visible kind patternsCore lint error with unused kind variable in data type return kind

Thanks, monoidal!

comment:4 Changed 9 months ago by RyanGlScott

It's worth noting that this Core Lint error only appears to occur when GHC constructs a wrapper for Prod. In other words, the following errors:

data F :: forall (cat1 :: ob1). ob1 -> Type where
  Prod :: forall u (a :: u). F a

But this does not error:

data F :: forall (cat1 :: ob1). ob1 -> Type where
  Prod :: F a

Since in the latter code, Prod won't need a wrapper, and its type will simply be forall {ob1} {cat1 :: ob1} (a :: ob1). F a. (Currently, there's no way to write that with GHC's explicit forall syntax, so pretty much any attempt to write the type of Prod using a forall will trigger this error.)

comment:5 Changed 9 months ago by RyanGlScott

Here's another way to trigger (what I believe to be) the same issue:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Bug where

import Data.Kind

type KindOf (a :: k) = k

data T :: forall j (a :: j). KindOf a -> Type where
  MkT :: forall k (b :: k). T b
$ /opt/ghc/8.6.3/bin/ghc Bug.hs -dcore-lint
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Tidy Core ***
<no location info>: warning:
    In the type ‘forall (a :: k_aVT[sk:1]) k (b :: k). T b’
    @ k_aVT[sk:1] is out of scope
*** Offending Program ***
$WMkT [InlPrag=INLINE[2]]
  :: forall (a :: k_aVT[sk:1]) k (b :: k). T b
[GblId[DataConWrapper],
 Caf=NoCafRefs,
 Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True,
         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)
         Tmpl= \ (@ (a_aWw :: k_aVT[sk:1]))
                 (@ k_XVV)
                 (@ (b_aVU :: k_XVV)) ->
                 MkT @ k_XVV @ a_aWw @ b_aVU}]
$WMkT
  = \ (@ (a_aWw :: k_aVT[sk:1])) (@ k_XVV) (@ (b_aVU :: k_XVV)) ->
      MkT @ k_XVV @ a_aWw @ b_aVU

<elided>

*** End of Offense ***


<no location info>: error: 
Compilation had errors

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

In 71e26a74/ghc:

Make candidateQTvs contain tyvar with zonked kinds

candidateQTyVars was failing to return fully-zonked
tyvars, and that made things fall over chaotically
when we try to sort them into a well-scoped telescope.
Result: Trac #15795

So I made candidateQTvs guarantee to have fully-zonked
tyvars (i.e. with zonked kinds).  That's a bit annoying
but not really difficult.

comment:7 Changed 9 months ago by simonpj

Test Case: tests/polykinds/T15795, T15795a

Great test cases thank you.

The cause was that candidateQTyVars was returning tyvars with unzonked kinds, and that meant we put the binders in the wrong dependency order. Once that happens, chaos results.

The fix is easy, but a bit tiresome. Richard you might want to look. The key point it this (in TcMType).

    go_tv dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) tv
      | tv `elemDVarSet` kvs = return dv  -- We have met this tyvar aleady
      | not is_dep
      , tv `elemDVarSet` tvs = return dv  -- We have met this tyvar aleady
      | otherwise
      = do { tv_kind <- zonkTcType (tyVarKind tv)
                 -- This zonk is annoying, but it is necessary, both to
                 -- ensure that the collected candidates have zonked kinds
                 -- (Trac #15795) and to make the naughty check
                 -- (which comes next) works correctly
           ; if intersectsVarSet bound (tyCoVarsOfType tv_kind)

Now from the two test cases we get the following results.

From comment:5 (immortalised as polykinds/T15795 we get

TYPE CONSTRUCTORS
  type synonym KindOf{2} :: forall k. k -> *
    roles nominal phantom
  data type T{3} :: forall j (a :: j). KindOf @j a -> *
    roles nominal nominal phantom
DATA CONSTRUCTORS
  MkT :: forall k (b :: k). T @k @(GHC.Types.Any @k) b

From comment:2 (immortalised as polykinds/T15795a we get

TYPE CONSTRUCTORS
  data type F{3} :: forall ob1 (cat1 :: ob1). ob1 -> *
    roles nominal nominal phantom
DATA CONSTRUCTORS
  Prod :: forall u (a :: u). F @u @(GHC.Types.Any @u) a

Note the use of Any, which I think is right.

Richard/Ryan: just check? Then close.

comment:8 Changed 9 months ago by goldfire

Resolution: fixed
Status: newclosed

Checked.

comment:9 Changed 8 months ago by Richard Eisenberg <rae@…>

In 17bd1635/ghc:

Visible kind application

Summary:
This patch implements visible kind application (GHC Proposal 15/#12045), as well as #15360 and #15362.
It also refactors unnamed wildcard handling, and requires that type equations in type families in Template Haskell be
written with full type on lhs. PartialTypeSignatures are on and warnings are off automatically with visible kind
application, just like in term-level.

There are a few remaining issues with this patch, as documented in
ticket #16082.

Includes a submodule update for Haddock.

Test Plan: Tests T12045a/b/c/TH1/TH2, T15362, T15592a

Reviewers: simonpj, goldfire, bgamari, alanz, RyanGlScott, Iceland_jack

Subscribers: ningning, Iceland_jack, RyanGlScott, int-index, rwbarton, mpickering, carter

GHC Trac Issues: `#12045`, `#15362`, `#15592`, `#15788`, `#15793`, `#15795`, `#15797`, `#15799`, `#15801`, `#15807`, `#15816`

Differential Revision: https://phabricator.haskell.org/D5229
Note: See TracTickets for help on using tickets.