[GHC] #13006: Possible program should type check but does not using Implicit Parameters and Vectors
#13006: Possible program should type check but does not using Implicit Parameters and Vectors -------------------------------------+------------------------------------- Reporter: clinton | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.2-rc2 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: -------------------------------------+------------------------------------- I think (but I'm not sure) that the following code should type check. This will require using the 'vector' package to illustrate this issue, sorry I couldn't create an example without it. Either uncommenting the explicit `m ()` signature or changing the type to the simpler `D m` data type will allow the code to compile. {{{ {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE KindSignatures #-} import Data.Vector.Unboxed.Mutable (MVector) import Control.Monad.Primitive (PrimMonad, PrimState) data D (x :: * -> *) type T m = MVector (PrimState m) Int --type T m = D m h :: forall m. PrimMonad m => T m -> m () h x = let f _ = (let ?v = x in g) {- :: m () -} in f undefined g :: (PrimMonad m , ?v :: T m) => m () g = undefined main = pure () }}} Alternatively, including `g` into the let binding as opposed to the top level will also compile: {{{ {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE KindSignatures #-} import Data.Vector.Unboxed.Mutable (MVector) import Control.Monad.Primitive (PrimMonad, PrimState) data D (x :: * -> *) type T m = MVector (PrimState m) Int --type T m = D m h :: forall m. PrimMonad m => T m -> m () h x = let f _ = (let ?v = x in g) {- :: m () -} g :: (PrimMonad m , ?v :: T m) => m () g = undefined in f undefined main = pure () }}} Perhaps this isn't a bug and has to do with the rank-2 type inside of Vector, but I'm just putting in this bug report to confirm. This is an issue as of 8.0.2-rc2. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13006 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13006: Possible program should type check but does not using Implicit Parameters and Vectors -------------------------------------+------------------------------------- Reporter: clinton | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.2-rc2 Resolution: invalid | 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 simonpj): * status: new => closed * resolution: => invalid Comment: In {{{ f _ = let ?v = x in g }}} what type did you expect `f` to have? GHC infers {{{ f :: forall a n. (...) => a -> n () }}} because `g :: forall m. (PrimMonad m, ?v :: T m) => m ()`. (I've used `n` instead of `m` in `f`'s type to emphasise that it is different to `m`. What is the `(...)`? The body of `f` has a call `g`, which gives rise to the constraints `(PrimMonad n, ?v :: T n)`. Alas the `?v` binding in f's RHS binds `?v :: T m` (since `x :: T m`), and that is no help in discharging `?v :: T n`. So we end up with {{{ f :: forall a n. (PrimMonad n, ?v :: T n) => n () }}} and hence the error. By adding the signature you make `f` monomorphic (`-XMonoLocalBinds` has the same effect) which solves the problem. Perhaps we should be more aggressive in reporting an error when functional dependencies can't be satisfied, but I think the program should indeed be rejected. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13006#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13006: Possible program should type check but does not using Implicit Parameters and Vectors -------------------------------------+------------------------------------- Reporter: clinton | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.2-rc2 Resolution: invalid | 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 clinton): Thank you for the explanation, but why does the code happily compile when `type T m = D m`? Your explanation above seems independent of the exact definition of `T`, so is there an alternate bug for the `type T m = D m` case where the code compiles when it shouldn't? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13006#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13006: Possible program should type check but does not using Implicit Parameters and Vectors -------------------------------------+------------------------------------- Reporter: clinton | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.2-rc2 Resolution: invalid | 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 simonpj): From the given `[G] ?v :: MVector (PrimState m) Int` and wanted `[G] ?v MVector (PrimState n) Int` we get the derived equality `[D] MVector (PrimState m) Int ~ MVector (PrimState n) Int`. Alas `PrimState` is a (non-injective) type family, so this does not tell us that `M ~ n`. In the simpler version, it does. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13006#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13006: Possible program should type check but does not using Implicit Parameters and Vectors -------------------------------------+------------------------------------- Reporter: clinton | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.2-rc2 Resolution: invalid | 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 clinton): Ah that makes sense presumably even injectivity won't help here as we can't derive `a ~ b` from `F a ~ F b`, even if F is injective yes? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13006#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13006: Possible program should type check but does not using Implicit Parameters and Vectors -------------------------------------+------------------------------------- Reporter: clinton | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.2-rc2 Resolution: invalid | 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 simonpj): On the contrary, if `F` is injective then we can indeed deduce `a ~ b` from `F a ~ F b`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13006#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13006: Possible program should type check but does not using Implicit Parameters and Vectors -------------------------------------+------------------------------------- Reporter: clinton | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.2-rc2 Resolution: invalid | 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 clinton): @simonpj: I'm not sure if I should put in a separate bug report or if I'm completely confused, but when I compile the following: {{{#!hs {-# LANGUAGE TypeFamilyDependencies #-} type family F x = t | t -> x myId :: (F a ~ F b) => a -> b myId = id main = pure () }}} I get the error: {{{ Could not deduce: a ~ b from the context: F a ~ F b }}} Isn't this what ticket #10833 discusses, namely that GHC does not derive `a ~ b` from `F a ~ F b`? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13006#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13006: Possible program should type check but does not using Implicit Parameters and Vectors -------------------------------------+------------------------------------- Reporter: clinton | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.2-rc2 Resolution: invalid | 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 simonpj): It depends what you mean by "derive". Injectivity gives rise to so-called "Derived equalities" which guide unification (often called "improvement"). They do not provide ''evidence'' in the sense of System FC. So, with your type family {{{ f :: F a -> F a f x = x }}} would not be reported as an ambiguous type; without the injectivity constraint it would. I wish there was a comprehensive writeup about this... it's too much folk lore. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13006#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC