[GHC] #13537: Adding underscore (m :: _) to pattern variable makes it fail
#13537: Adding underscore (m :: _) to pattern variable makes it fail -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | 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: -------------------------------------+------------------------------------- This works fine {{{#!hs {-# Language RankNTypes, TypeOperators, KindSignatures, GADTs, ScopedTypeVariables, PolyKinds #-} import Data.Kind data CodTy :: (k -> Type) -> Type where CodTy :: { runCodTy :: (forall r. (f ty -> r) -> r) } -> CodTy f type f ~> g = forall xx. f xx -> g xx fmap' :: (f ~> f') -> (CodTy f -> CodTy f') fmap' f (CodTy m) = CodTy $ \ c -> m (c . f) }}} but adding {{{#!hs fmap' f (CodTy (m :: _)) = CodTy $ \ c -> m (c . f) }}} makes it fail (also fails without `PolyKinds`) {{{ $ ghci -ignore-dot-ghci tNT2.hs GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( tNT2.hs, interpreted ) tNT2.hs:11:22: error: • Found type wildcard ‘_’ standing for ‘(f ty -> r0) -> r0’ Where: ‘r0’ is an ambiguous type variable ‘f’ is a rigid type variable bound by the type signature for: fmap' :: forall k (f :: k -> *) (f' :: k -> *). f ~> f' -> CodTy f -> CodTy f' at tNT2.hs:10:10 ‘ty’ is a rigid type variable bound by a pattern with constructor: CodTy :: forall k (f :: k -> *) (ty :: k). (forall r. (f ty -> r) -> r) -> CodTy f, in an equation for ‘fmap'’ at tNT2.hs:11:10 ‘k’ is a rigid type variable bound by the type signature for: fmap' :: forall k (f :: k -> *) (f' :: k -> *). f ~> f' -> CodTy f -> CodTy f' at tNT2.hs:10:10 To use the inferred type, enable PartialTypeSignatures • In a pattern type signature: _ In the pattern: m :: _ In the pattern: CodTy (m :: _) • Relevant bindings include f :: f ~> f' (bound at tNT2.hs:11:7) fmap' :: f ~> f' -> CodTy f -> CodTy f' (bound at tNT2.hs:11:1) tNT2.hs:11:46: error: • Couldn't match type ‘r0’ with ‘r’ because type variable ‘r’ would escape its scope This (rigid, skolem) type variable is bound by a type expected by the context: (f' ty -> r) -> r at tNT2.hs:11:28-51 Expected type: f ty -> r0 Actual type: f ty -> r • In the first argument of ‘m’, namely ‘(c . f)’ In the expression: m (c . f) In the second argument of ‘($)’, namely ‘\ c -> m (c . f)’ • Relevant bindings include c :: f' ty -> r (bound at tNT2.hs:11:38) m :: (f ty -> r0) -> r0 (bound at tNT2.hs:11:17) Failed, modules loaded: none. Prelude> }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13537 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13537: Adding underscore (m :: _) to pattern variable makes it fail -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: 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 Iceland_jack): And giving `\c -> m (c . d)` a name (without a type signature, I'm don't have enough bravery to attempt that so early in the morning) doesn't work, I don't know if intended behaviour or not {{{#!hs fmap' :: (f ~> f') -> (CodTy f -> CodTy f') fmap' f (CodTy m) = CodTy a where a c = m (c . f) fmap' f (CodTy m) = let a c = m (f . g) in CodTy a fmap' f (CodTy m) = do let a c = m (f . g) CodTy a }}} Okay never mind I worked it out, this works {{{#!hs fmap' :: forall f f'. (f ~> f') -> (CodTy f -> CodTy f') fmap' f (CodTy (m :: forall r'. (f ty -> r') -> r')) = CodTy a where a :: forall r. (f' ty -> r) -> r a c = m (c . f) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13537#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13537: Adding underscore (m :: _) to pattern variable makes it fail -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: 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): Consider this: {{{ data T where MkT :: (forall a. a->a) -> T f (MkT (g :: Int->Int)) = .. }}} Is this ok? Well yes. The argument of `MkT` has type `forall a. a->a`, but it can be instantiated to the type `Int->Int`, so we can legitimately end up with `g :: Int->Int`. In FC it'd look like {{{ f x = case x of MkT (g2 :: forall a.a->a) -> let g::Int->Int = g2 @ Int in ... }}} Now you want to force the type of the pattern to be `_`. But since GHC only supports predicative polymorphism, `_` must be a monotype. So GHC instantiates `forall a. a->a` to `alpha -> alpha` (for some new unification variable alpha), and proceeds. And that is what you see in the first message "Found type wildcard...". But alas of course, in your example we need `m` to be a polytype, and making it a monotype leads to a subsequent rather obscure error message. Does that help? Is there some way we could improve the user manual? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13537#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13537: Adding underscore (m :: _) to pattern variable makes it fail -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: invalid | Keywords: 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 Iceland_jack): * status: new => closed * resolution: => invalid Comment: Replying to [comment:2 simonpj]:
Now you want to force the type of the pattern to be `_`. But since GHC only supports predicative polymorphism, `_` must be a monotype. So GHC instantiates `forall a. a->a` to `alpha -> alpha` (for some new unification variable alpha), and proceeds.
I suspected this was related to impredicativity. As a user I expected transforming the pattern `m` to `(m :: _)` would have no effect since it binds nothing (the compiler ''could'' special-case it, even though it brings no benefits).
Does that help?
Is there some way we could improve the user manual?
Yes it helps. I think the impredicative polymorphism entry is rather good, thanks for the explanation. To be clear, this is also expected? Closing the ticket {{{#!hs -- Works tId :: T -> T tId (MkT g) = MkT g -- Fails tId :: T -> T tId (MkT g) = MkT g' where g' = g }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13537#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13537: Adding underscore (m :: _) to pattern variable makes it fail -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: invalid | Keywords: 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):
To be clear, this is also expected?
Yes, but for an entirely different reason. The local binding `g' = g` is not generalised, because with `GADTs` on (which you presumably have) we have `MonoLocalBinds` on too. So `g'` is no generalised; and hence it's rejected as an argumen to `MkT`. If you gave `g'` a type signature you'd be fine. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13537#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13537: Adding underscore (m :: _) to pattern variable makes it fail -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: invalid | Keywords: 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 Iceland_jack): Thank you, consider this answered. ---- I was reifying `(forall ty. STy ty -> r) -> r` from [https://github.com/goldfirere/glambda/blob/ex3/src/Language/Glambda/Type.hs#... Richard's Glambda] {{{#!hs refineTy :: Ty -> (forall ty. STy ty -> r) -> r refineTy (ty1 `Arr` ty2) k = refineTy ty1 $ \sty1 -> refineTy ty2 $ \sty2 -> k (sty1 `SArr` sty2) refineTy IntTy k = k SIntTy refineTy BoolTy k = k SBoolTy }}} If this were a regular continuation / codensity monad we could rewrite it to {{{#!hs refineTy = \case Arr a b -> liftA2 SArr (refine a) (refine b) IntTy -> pure SIntTy BoolTy -> pure SBoolTy }}} but it seems to be a functor from a ''functor'' category, so I'm trying to figure out where it fits in the hierarchy. Thanks. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13537#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC