[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
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
#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]: 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
#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