Opened 10 months ago
Closed 10 months ago
#14584 closed bug (fixed)
Core Lint error
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 8.2.1 |
Keywords: | TypeInType, DeferredTypeErrors | Cc: | goldfire |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | testsuite/tests/partial-sigs/should_fail/T14584, T14584a |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
{-# Language PartialTypeSignatures #-} {-# Language TypeFamilyDependencies, KindSignatures #-} {-# Language PolyKinds #-} {-# Language DataKinds #-} {-# Language TypeFamilies #-} {-# Language RankNTypes #-} {-# Language NoImplicitPrelude #-} {-# Language FlexibleContexts #-} {-# Language MultiParamTypeClasses #-} {-# Language GADTs #-} {-# Language ConstraintKinds #-} {-# Language FlexibleInstances #-} {-# Language TypeOperators #-} {-# Language ScopedTypeVariables #-} {-# Language DefaultSignatures #-} {-# Language FunctionalDependencies #-} {-# Language UndecidableSuperClasses #-} {-# Language UndecidableInstances #-} {-# Language TypeInType #-} {-# Language AllowAmbiguousTypes #-} {-# Language InstanceSigs, TypeApplications #-} import Data.Monoid import Data.Kind data family Sing (a::k) class SingKind k where type Demote k = (res :: Type) | res -> k fromSing :: Sing (a::k) -> Demote k class SingI (a::k) where sing :: Sing a data ACT :: Type -> Type -> Type data MHOM :: Type -> Type -> Type type m ·- a = ACT m a -> Type type m ·-> m' = MHOM m m' -> Type class Monoid m => Action (act :: m ·- a) where act :: m -> (a -> a) class (Monoid m, Monoid m') => MonHom (mhom :: m ·-> m') where monHom :: m -> m' data MonHom_Distributive m :: (m ·- a) -> (a ·-> a) type Good k = (Demote k ~ k, SingKind k) instance (Action act, Monoid a, Good m) => MonHom (MonHom_Distributive m act :: a ·-> a) where monHom :: a -> a monHom = act @_ @_ @act (fromSing @m (sing @m @a :: Sing _)) where
fails on 8.2.1 and 8.3.20171208 when passed -fdefer-type-errors -dcore-lint
, full log attached
$ ghci -ignore-dot-ghci -fdefer-type-errors -dcore-lint 146-bug.hs GHCi, version 8.3.20171208: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 146-bug.hs, interpreted ) *** Core Lint errors : in result of Desugar (after optimization) *** <no location info>: warning: In the expression: fromSing @ m_a2Ju ...
Attachments (1)
Change History (12)
Changed 10 months ago by
comment:1 Changed 10 months ago by
Keywords: | TypeInType DeferredTypeErrors added |
---|
comment:2 Changed 10 months ago by
Cc: | goldfire added |
---|
comment:3 Changed 10 months ago by
I've reduced to:
{-# Language PartialTypeSignatures #-} {-# Language KindSignatures #-} {-# Language PolyKinds #-} {-# Language ScopedTypeVariables #-} {-# Language AllowAmbiguousTypes #-} {-# Language TypeApplications #-} f :: forall m. () f = id @m :: _
and as previously ghci -ignore-dot-ghci -fdefer-type-errors -dcore-lint 146-bug.hs
gives a Core Lint error; I've checked 8.2.1 but not HEAD.
comment:4 Changed 10 months ago by
Why doesn't co2
float out? We really shouldn't float co1
out if we don't float co2
out. The fact that it works without deferred type errors is just a fluke, really. (What if co2
ends up being filled in with a coercion that mentions x
?)
I think this can be fixed just by adding a little more logic to the float-out code. Unfortunately, it also means that we need to calculate floating-out in dependency order (so we can process co2
before even looking at co1
. It makes the floating-out code a little more intricate, but the complication should be quite local.
Does that sound reasonable?
comment:5 Changed 10 months ago by
What if co2 ends up being filled in with a coercion that mentions x?
Excellent question! But even a more complicated floating isn't enough. Suppose co2
is actually solved. Then its binding will live in the inner implication; so we then can't float co1
. And if that solved binding did mention x
, then we should presumably not float co1
. Yikes. This works today because: if co2
is solved, when we zonk co1
we'll see all the free vars of co1
(because of the update in place stuff).
In truth, if coercions generated bindings in the implication, we'd have to float them too, assuming none of them mention the skolemised variables.
Bottom line: it seems delicate, but yes perhaps doing transitive capture would nail it.
comment:6 Changed 10 months ago by
...or not. Monoidal's example is amazing. Here's the constraint we get (before simplifying it):
simplifyTop { wanted = WC {wc_impl = Implic { TcLevel = 2 Skolems = k_aGF[sk:2] (m_aGG[sk:2] :: k_aGF[sk:2]) No-eqs = False Status = Unsolved Given = Wanted = WC {wc_simple = [WD] hole{aGP} {0}:: ((m_aGG[sk:2] |> {aGN}) -> (m_aGG[sk:2] |> {aGN}) :: *) GHC.Prim.~# (() :: *) (CNonCanonical) wc_impl = Implic { TcLevel = 3 Skolems = No-eqs = False Status = Unsolved Given = Wanted = WC {wc_simple = [D] _ {0}:: (m_aGG[sk:2] |> {aGN}) -> (m_aGG[sk:2] |> {aGN}) (CHoleCan: TypeHole(_)) [WD] hole{aGN} {0}:: (k_aGF[sk:2] :: *) GHC.Prim.~# (* :: *) (CNonCanonical)} Binds = EvBindsVar<aGO> Needed = [] the inferred type of <expression>_02y :: w_aGJ[tau:3] }} Binds = EvBindsVar<aGQ> Needed = [] the type signature for: f :: forall k (m :: k). () }}
Notice that the coercion {aGN}
is a Wanted inside the inner implication constraint, but is used in a constraint (for {aGP}
) outside that implication. No amount of floating is going to put that right!
comment:7 Changed 10 months ago by
We don't even need a partial type signature. This gives a similar Lint error (when compiled with -fdefer-type-errrors
:
g :: forall m. () g = let h = id @m in h
comment:8 Changed 10 months ago by
comment:6 is frightening. I can look into this in due course, but do you see how on earth that happens? I wonder if that's a separate bug.
comment:11 Changed 10 months ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Test Case: | → testsuite/tests/partial-sigs/should_fail/T14584, T14584a |
Blimey. That rabbit-hole was a lot deeper than I expected.
Yurgh. I don't yet understand the details, but what is happening is something like this. We have an implication constraint
Here
co2
is an ultimately-unsolved kind coercion. We floatco1
out of the implication and unify withalpha
. Then inTcErrors
we make evidence forco2
using a call toerror
, bound in theEvBinds
for the implication.But alas the scope of the binding for
co2
is just the term enclosed by the implication constraint. But the use ofco2
has escaped, in the typealpha
.Yikes. This only shows up with deferred type errors, because normally we don't make term-level bindings for coercions; instead we just side-effect them right into the coercions they are used in, which just happens to work even in the "escaping" case. But with deferred type errors we need to force a term-level error, and to do so in as narrow a scope as possible.
I'd like a smaller test case to show this up.
I really do not know how to solve this. It's all because of those pesky casts inside types! Richard, your advice would be valuable here.