[GHC] #12526: regression in type inference with respect to type families
#12526: regression in type inference with respect to type families -------------------------------------+------------------------------------- Reporter: Lemming | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.0.2 Component: Compiler | Version: 8.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The following bug is present in ghc-8.0.1.20160725, ghc-8.0.1.20160822 (ghc-8.0.2) and ghc-8.1.20160819 (ghc-head) and was not there in ghc-8.0.1. When compiling the head version of synthesizer-llvm package from http://code.haskell.org/synthesizer/llvm/ I get the following error: {{{ src/Synthesizer/LLVM/Server/CausalPacked/Instrument.hs:296:23: error: • Couldn't match type ‘Synthesizer.Causal.Class.ProcessOf t0’ with ‘CausalP.T (SampleRate Real, ())’ Expected type: CausalP.T (SampleRate Real, ()) (Serial.T (LLVM.Value (LLVM.Vector (TypeNum.Pos Type.Data.Num.Decimal.Digit.Dec4 TypeNum.EndDesc) Float)), (Serial.Value (TypeNum.Pos Type.Data.Num.Decimal.Digit.Dec4 TypeNum.EndDesc) Real, VectorValue)) (Serial.T (LLVM.Value (LLVM.Vector (TypeNum.Pos Type.Data.Num.Decimal.Digit.Dec4 TypeNum.EndDesc) Float))) Actual type: Synthesizer.Causal.Class.ProcessOf t0 (Serial.T (LLVM.Value (LLVM.Vector (TypeNum.Pos Type.Data.Num.Decimal.Digit.Dec4 TypeNum.EndDesc) Float)), (Serial.Value (TypeNum.Pos Type.Data.Num.Decimal.Digit.Dec4 TypeNum.EndDesc) Float, Serial.Value (TypeNum.Pos Type.Data.Num.Decimal.Digit.Dec4 TypeNum.EndDesc) Float)) (Serial.T (LLVM.Value (LLVM.Vector (TypeNum.Pos Type.Data.Num.Decimal.Digit.Dec4 TypeNum.EndDesc) Float))) The type variable ‘t0’ is ambiguous • In the first argument of ‘($&)’, namely ‘osci’ In the second argument of ‘liftA2’, namely ‘(osci $& shapeCtrl &|& (expo &|& fmap Stereo.left freqs))’ In the expression: liftA2 Stereo.cons (osci $& shapeCtrl &|& (expo &|& fmap Stereo.left freqs)) (osci $& shapeCtrl &|& (negate expo &|& fmap Stereo.right freqs)) • Relevant bindings include osci :: Synthesizer.Causal.Class.ProcessOf t0 (Serial.T (LLVM.Value (LLVM.Vector (TypeNum.Pos Type.Data.Num.Decimal.Digit.Dec4 TypeNum.EndDesc) Float)), (Serial.Value (TypeNum.Pos Type.Data.Num.Decimal.Digit.Dec4 TypeNum.EndDesc) Float, Serial.Value (TypeNum.Pos Type.Data.Num.Decimal.Digit.Dec4 TypeNum.EndDesc) Float)) (Serial.T (LLVM.Value (LLVM.Vector (TypeNum.Pos Type.Data.Num.Decimal.Digit.Dec4 TypeNum.EndDesc) Float))) (bound at src/Synthesizer/LLVM/Server/CausalPacked/Instrument.hs:294:19) }}} The type for `t0` should be known and then the type checker should be able to check that `ProcessOf t0` equals `CausalP.T`. It did so in earlier versions but now fails on that part. I still have to reduce that example, but for now I want to alert you that there seems to be a regression in the type inference. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12526> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12526: regression in type inference with respect to type families -------------------------------------+------------------------------------- Reporter: Lemming | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.2 Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by mpickering): * priority: normal => highest -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12526#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12526: regression in type inference with respect to type families -------------------------------------+------------------------------------- Reporter: Lemming | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.2 Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Lemming): It is pretty strange: If I compile synthesizer-llvm in one go then it can be compiled by ghc-8.0.1. Then I alter the problematic module (update of date is enough), re-compile, and now surprisingly also ghc-8.0.1 produces the same error message. That is, the error already existed in ghc-8.0.1 but was not always triggered. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12526#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12526: regression in type inference with respect to type families -------------------------------------+------------------------------------- Reporter: Lemming | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.2 Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by mpickering): * cc: niteria (added) Comment: It seems that this might be related to the work that Bartosz has done in making GHC more deterministic. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12526#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12526: regression in type inference with respect to type families -------------------------------------+------------------------------------- Reporter: Lemming | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.2 Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by niteria):
It seems that this might be related to the work that Bartosz has done in making GHC more deterministic.
That is, the error already existed in ghc-8.0.1 but was not always triggered.
Most of the determinism patches were merged *after* ghc-8.0.1, so it sounds unlikely. My best bet would be that some exposed thing isn't recorded in the interface file. Lemming: Can you provide step by step repro? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12526#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12526: regression in type inference with respect to type families -------------------------------------+------------------------------------- Reporter: Lemming | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.2 Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: 10634 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Lemming): * related: => 10634 Comment: Replying to [comment:4 niteria]:
It seems that this might be related to the work that Bartosz has done in making GHC more deterministic.
That is, the error already existed in ghc-8.0.1 but was not always triggered.
Most of the determinism patches were merged *after* ghc-8.0.1, so it sounds unlikely.
Why? GHC-8.0.1 showed the error sometimes, GHC-8.0.2 shows it always. mpickering's guess matches perfectly.
Lemming: Can you provide step by step repro?
I am currently reducing the example. It looks like another instance of the fake injective type functions problem. https://ghc.haskell.org/trac/ghc/ticket/10634 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12526#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12526: regression in type inference with respect to type families -------------------------------------+------------------------------------- Reporter: Lemming | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.2 Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: 10634 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Lemming): * Attachment "InjectiveInference.hs" added. A minimal self-contained example demonstrating the problem -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12526> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12526: regression in type inference with respect to type families -------------------------------------+------------------------------------- Reporter: Lemming | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.2 Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: 10634 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Lemming): The `let` in `ping` is essential for triggering the bug. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12526#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12526: regression in type inference with respect to type families -------------------------------------+------------------------------------- Reporter: Lemming | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.2 Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: 10634 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by niteria): This reproduces in HEAD (from Aug 9) with: {{{ InjectiveInference.hs:35:8: error: • Couldn't match type ‘ProcessOf t0’ with ‘Causal’ Expected type: Causal Float Float Actual type: ProcessOf t0 Float Float The type variable ‘t0’ is ambiguous • In the first argument of ‘($&)’, namely ‘osci’ In the expression: osci $& frequencies In the expression: let osci = shapeModOsci in osci $& frequencies • Relevant bindings include osci :: forall y. ProcessOf t0 Float y (bound at InjectiveInference.hs:34:8) }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12526#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12526: regression in type inference with respect to type families -------------------------------------+------------------------------------- Reporter: Lemming | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.2 Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: 10634 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by niteria): Adding: {{{ {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE FlexibleContexts #-} }}} produces a different message: {{{ InjectiveInference.hs:36:8: error: • Could not deduce: ProcessOf t0 ~ ProcessOf t from the context: CausalProcess (ProcessOf t) bound by the inferred type for ‘osci’: CausalProcess (ProcessOf t) => ProcessOf t Float y at InjectiveInference.hs:36:8-26 Expected type: ProcessOf t Float y Actual type: ProcessOf t0 Float y NB: ‘ProcessOf’ is a type function, and may not be injective The type variable ‘t0’ is ambiguous • In the ambiguity check for the inferred type for ‘osci’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes When checking the inferred type osci :: forall y (t :: * -> *). CausalProcess (ProcessOf t) => ProcessOf t Float y In the expression: let osci = shapeModOsci in osci $& frequencies }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12526#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12526: regression in type inference with respect to type families -------------------------------------+------------------------------------- Reporter: Lemming | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.2 Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: 10634 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Here is a yet simpler version of the problem {{{ {-# LANGUAGE TypeFamilies, MonoLocalBinds #-} module T12526 where type family P (s :: * -> *) :: * -> * -> * type instance P Signal = Causal type family S (p :: * -> * -> *) :: * -> * type instance S Causal = Signal class (P (S p) ~ p) => CP p instance CP Causal data Signal a = Signal data Causal a b = Causal shapeModOsci :: CP p => p Float Float shapeModOsci = undefined f :: Causal Float Float -> Bool f = undefined -- This fails ping :: Bool ping = let osci = shapeModOsci in f osci -- This works -- ping :: Bool -- ping = f shapeModOsci }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12526#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12526: regression in type inference with respect to type families -------------------------------------+------------------------------------- Reporter: Lemming | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.2 Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: 10634 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I spent some time finding out what is going on here. * We typecheck the binding for `osci` with generalisation (despite `NoMonoBinds`) because the RHS has no locally-bound free variables. * But `osci` triggers the monomorphism restriction because of the `(CP t)` constraint. * So from `osci`s binding we initially get (where `pp` is a unification variable) {{{ osci :: pp Float Float Constraints: CP pp }}} * However, during inference of `osci`'s type we try to simplify those constraints (`simplifyInfer`). So we get {{{ [W] CP pp --> add derived superclass constraints [W] CP pp [D] pp ~ P (S pp) But we flatten those constraints to get --> flatten (the fuv1/2 are flatten-meta-vars) [W] CP pp [D] pp ~ fuv1 [D] S pp ~ fuv2 (CFunEqCan) [D] P fuv2 ~ fuv1 (CFunEqCan) --> Now (here is the problem) we unify pp := fuv1 [W] CP fuv1 [D] S fuv1 ~ fuv2 (CFunEqCan) [D] P fuv2 ~ fuv1 (CFunEqCan) --> Nothing further happens, so we unflatten to get fuv1 := P fuv2 [W] CP (P fuv2) [D] P (S fuv2) ~ fuv2 Discarding the derived constraint we have ended up with osci :: P fuv2 Float Float Constaints: CP (P fuv2) }}} * But replacinng `pp := P fuv2` is bad, because in the call `f osci`, we now get {{{ [W] Causal Float Float ~ P fuv2 Float Float }}} which leads to `P fuv2 ~ Causal`, which doesn't tell us how to choose `fuv2`. If we had only left it alone, we'd have had {{{ [W] Causal Float Float ~ pp Float Float }}} which tells us `p := Causal` and everything gets solved. I have not investigated why it worked before, but it's clearly terribly delicate. For now I'm just recording the breadcrumbs. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12526#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12526: regression in type inference with respect to type families -------------------------------------+------------------------------------- Reporter: Lemming | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.2 Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: 10634 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Lemming): Replying to [comment:9 simonpj]:
Here is a yet simpler version of the problem
Thank you for the simplification! I guess we can also drop the type parameters of `Signal` and `Causal`. For now I have solved the problem in my package by adding type signatures to the let binding. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12526#comment:11> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12526: regression in type inference with respect to type families -------------------------------------+------------------------------------- Reporter: Lemming | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: 10634 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * milestone: 8.0.2 => 8.2.1 Comment: I am in the middle of an upheaval of the constraint solver that fixes this among other things. But the change is too big to put in the 8.0.2 branch. So I suggest we re-milestone for 8.2, and treat this as something to work- around with 8.0.2. The workaround is simple, as comment:11 says: a type signature seems to do the job. I think it's a fluke that it worked before. Is that acceptable? I think it'll be hard to fix in 8.0.2. Yell if that'd be really bad for you. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12526#comment:12> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12526: regression in type inference with respect to type families -------------------------------------+------------------------------------- Reporter: Lemming | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #10634 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Lemming): * related: 10634 => #10634 Comment: I am ok with defering the solution to 8.2. These simulated injective type functions seem to be a constant source of trouble. How do other people cope with them? Are they all using real injective type functions instead? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12526#comment:13> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12526: regression in type inference with respect to type families -------------------------------------+------------------------------------- Reporter: Lemming | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #10634 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"1eec1f21268af907f59b5d5c071a9a25de7369c7/ghc" 1eec1f21/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="1eec1f21268af907f59b5d5c071a9a25de7369c7" Another major constraint-solver refactoring This patch takes further my refactoring of the constraint solver, which I've been doing over the last couple of months in consultation with Richard. It fixes a number of tricky bugs that made the constraint solver actually go into a loop, including Trac #12526 Trac #12444 Trac #12538 The main changes are these * Flatten unification variables (fmvs/fuvs) appear on the LHS of a tvar/tyvar equality; thus fmv ~ alpha and not alpha ~ fmv See Note [Put flatten unification variables on the left] in TcUnify. This is implemented by TcUnify.swapOverTyVars. * Don't reduce a "loopy" CFunEqCan where the fsk appears on the LHS: F t1 .. tn ~ fsk where 'fsk' is free in t1..tn. See Note [FunEq occurs-check principle] in TcInteract This neatly stops some infinite loops that people reported; and it allows us to delete some crufty code in reduce_top_fun_eq. And it appears to be no loss whatsoever. As well as fixing loops, ContextStack2 and T5837 both terminate when they didn't before. * Previously we generated "derived shadow" constraints from Wanteds, but we could (and sometimes did; Trac #xxxx) repeatedly generate a derived shadow from the same Wanted. A big change in this patch is to have two kinds of Wanteds: [WD] behaves like a pair of a Wanted and a Derived [W] behaves like a Wanted only See CtFlavour and ShadowInfo in TcRnTypes, and the ctev_nosh field of a Wanted. This turned out to be a lot simpler. A [WD] gets split into a [W] and a [D] in TcSMonad.maybeEmitShaodow. See TcSMonad Note [The improvement story and derived shadows] * Rather than have a separate inert_model in the InertCans, I've put the derived equalities back into inert_eqs. We weren't gaining anything from a separate field. * Previously we had a mode for the constraint solver in which it would more aggressively solve Derived constraints; it was used for simplifying the context of a 'deriving' clause, or a 'default' delcaration, for example. But the complexity wasn't worth it; now I just make proper Wanted constraints. See TcMType.cloneWC * Don't generate injectivity improvement for Givens; see Note [No FunEq improvement for Givens] in TcInteract * solveSimpleWanteds leaves the insolubles in-place rather than returning them. Simpler. I also did lots of work on comments, including fixing Trac #12821. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12526#comment:14> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#12526: regression in type inference with respect to type families -------------------------------------+------------------------------------- Reporter: Lemming | Owner: Type: bug | Status: closed Priority: highest | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.1 checker) | Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T12526 Blocked By: | Blocking: Related Tickets: #10634 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * testcase: => indexed-types/should_compile/T12526 * status: new => closed * resolution: => fixed -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12526#comment:15> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC