#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)
Change History (10)
Changed 11 months ago by
comment:1 Changed 9 months ago by
Cc: | mnguyen removed |
---|---|
Keywords: | TypeInType added; TypeApplications removed |
comment:2 Changed 9 months ago by
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
Summary: | Core lint error with visible kind patterns → Core lint error with unused kind variable in data type return kind |
---|
Thanks, monoidal!
comment:4 Changed 9 months ago by
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
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:7 Changed 9 months ago by
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.
This has nothing to do with visible kind application. This fails the same way: