[GHC] #14584: Core Lint error

GHC

15 Dec 2017 15 Dec '17

12:07 p.m.

#14584: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# 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 ... }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14584 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

Show replies by date

GHC

15 Dec 15 Dec

12:08 p.m.

GHC

12:16 p.m.

#14584: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType, | DeferredTypeErrors Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * keywords: => TypeInType, DeferredTypeErrors -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14584#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

GHC

19 Dec 19 Dec

7 a.m.

#14584: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType, | DeferredTypeErrors Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * cc: goldfire (added) Comment: Yurgh. I don't yet understand the details, but what is happening is something like this. We have an implication constraint {{{ forall x[2]. [W] co1: alpaha[1] ~ ty |> co2 [W] co2: k1 ~ * }}} Here `co2` is an ultimately-unsolved kind coercion. We float `co1` out of the implication and unify with `alpha`. Then in `TcErrors` we make evidence for `co2` using a call to `error`, bound in the `EvBinds` for the implication. But alas the scope of the binding for `co2` is just the term enclosed by the implication constraint. But the use of `co2` has escaped, in the type `alpha`. 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14584#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

GHC

7:18 p.m.

#14584: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType, | DeferredTypeErrors Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by monoidal): I've reduced to: {{{ {-# Language PartialTypeSignatures #-} {-# Language KindSignatures #-} {-# Language PolyKinds #-} {-# Language ScopedTypeVariables #-} {-# Language AllowAmbiguousTypes #-} {-# Language TypeApplications #-} data Sing (a :: *) = X f :: forall m a. Sing a f = X @m :: Sing _ }}} 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14584#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

GHC

8:52 p.m.

#14584: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType, | DeferredTypeErrors Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14584#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

GHC

20 Dec 20 Dec

5:20 a.m.

#14584: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType, | DeferredTypeErrors Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):

...

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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14584#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

GHC

5:21 a.m.

#14584: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType, | DeferredTypeErrors Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): ...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 a constraint (for `{aGP}`) outside that implication. No amount of floating is going to put that right! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14584#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

GHC

5:25 a.m.

#14584: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType, | DeferredTypeErrors Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): 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 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14584#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

GHC

9:19 a.m.

#14584: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType, | DeferredTypeErrors Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14584#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

GHC

21 Dec 21 Dec

9:55 a.m.

#14584: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType, | DeferredTypeErrors Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones ): In [changeset:"f5cf9d1a1b198edc929e1fa96c6d841d182fe766/ghc" f5cf9d1a/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="f5cf9d1a1b198edc929e1fa96c6d841d182fe766" Fix floating of equalities This rather subtle patch fixes Trac #14584. The problem was that we'd allowed a coercion, bound in a nested scope, to escape into an outer scope. The main changes are * TcSimplify.floatEqualities takes more care when floating equalities to make sure we don't float one out that mentions a locally-bound coercion. See Note [What prevents a constraint from floating] * TcSimplify.emitResidualConstraints (which emits the residual constraints in simplifyInfer) now avoids burying the constraints for escaping CoVars inside the implication constraint. * Since I had do to this stuff with CoVars, I moved the fancy footwork about not quantifying over CoVars from TcMType.quantifyTyVars to its caller TcSimplify.decideQuantifiedTyVars. I think its other callers don't need to worry about all this CoVar stuff. This turned out to be surprisigly tricky, and took me a solid day to get right. I think the result is reasonably neat, though, and well documented with Notes. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14584#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

GHC

9:55 a.m.

#14584: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType, | DeferredTypeErrors Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones ): In [changeset:"a492af06d3264530d134584f22ffb726a16c78ec/ghc" a492af06/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="a492af06d3264530d134584f22ffb726a16c78ec" Refactor coercion holes In fixing Trac #14584 I found that it would be /much/ more convenient if a "hole" in a coercion (much like a unification variable in a type) acutally had a CoVar associated with it rather than just a Unique. Then I can ask what the free variables of a coercion is, and get a set of CoVars including those as-yet-un-filled in holes. Once that is done, it makes no sense to stuff coercion holes inside UnivCo. They were there before so we could know the kind and role of a "hole" coercion, but once there is a CoVar we can get that info from the CoVar. So I removed HoleProv from UnivCoProvenance and added HoleCo to Coercion. In summary: * Add HoleCo to Coercion and remove HoleProv from UnivCoProvanance * Similarly in IfaceCoercion * Make CoercionHole have a CoVar in it, not a Unique * Make tyCoVarsOfCo return the free coercion-hole variables as well as the ordinary free CoVars. Similarly, remember to zonk the CoVar in a CoercionHole We could go further, and remove CoercionHole as a distinct type altogther, just collapsing it into HoleCo. But I have not done that yet. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14584#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

GHC

9:59 a.m.

#14584: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: fixed | Keywords: TypeInType, | DeferredTypeErrors 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: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * testcase: => testsuite/tests/partial-sigs/should_fail/T14584, T14584a * resolution: => fixed Comment: Blimey. That rabbit-hole was a lot deeper than I expected. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14584#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

2708

Age (days ago)

2714

Last active (days ago)

List overview

Download

12 comments

1 participants

[GHC] #14584: Core Lint error

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

tags

participants (1)