[GHC] #7916: PolyKinds without type signatures
#7916: PolyKinds without type signatures --------------------------------------+------------------------------------- Reporter: monoidal | Owner: Type: bug | Status: new Priority: normal | Component: Compiler (Type checker) Version: 7.7 | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC rejects valid program | Blockedby: Blocking: | Related: --------------------------------------+------------------------------------- Consider {{{ {-# LANGUAGE PolyKinds, ExplicitForAll #-} f :: forall (m :: k -> *) (a :: k). m a -> m a f = id g = f }}} I would expect GHC to infer the same type for `g` as for `f`. However, it gives the AnyK kind, and `g` is not possible to use: {{{ ghci -Wall X.hs ... X.hs:5:1: Warning: Top-level binding with no type signature: g :: forall (m :: AnyK -> *) (a :: AnyK). m a -> m a Ok, modules loaded: Main. *Main> g "a" <interactive>:2:1: Kind incompatibility when matching types: a0 :: AnyK Char :: * In the first argument of ‛print’, namely ‛it’ In a stmt of an interactive GHCi command: print it }}} -- Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7916> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#7916: PolyKinds without type signatures ----------------------------------------+----------------------------------- Reporter: monoidal | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.7 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: GHC rejects valid program Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: | ----------------------------------------+----------------------------------- Changes (by simonpj): * difficulty: => Unknown Comment: Crumbs. Absolutely right. Your example identifies a real bug in the quantification over kinds. I've spent part of today fixing it, happily by simplifying the type inference engine! Patch coming, but not till Monday. -- Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7916#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#7916: PolyKinds without type signatures ----------------------------------------+----------------------------------- Reporter: monoidal | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.7 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: GHC rejects valid program Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: | ----------------------------------------+----------------------------------- Comment(by simonpj@…): commit ce89bdecac936bff9378b60f156d8c560c3c1380 {{{ Author: Simon Peyton Jones <simonpj@microsoft.com> Date: Tue May 21 12:29:54 2013 +0100 Simplify kind generalisation, and fix Trac #7916 A buglet that exposed an opportunity for some welcome refactoring and simplification. Main changes * TcMType.zonkQuantifiedTyVars is replaced by quantifyTyVars, which does a bit more zonking (so that its clients do not need to) * TcHsType.kindGeneralise becomes a bit simpler, and hands off to quantifyTyVars * A bit of simplification of the hacky code in TcTyClsDcls.tcConDecl, where we figure out how to generalise the data constructor's type * Improve the error message from badExistential when a constructor has an existential type, by printing the offending type * Some consequential simplification in simplifyInfer. compiler/basicTypes/VarSet.lhs | 4 +- compiler/typecheck/TcHsType.lhs | 22 +-- compiler/typecheck/TcMType.lhs | 324 +++++++++++++++++++---------------- compiler/typecheck/TcRules.lhs | 14 +- compiler/typecheck/TcSimplify.lhs | 66 +++----- compiler/typecheck/TcSplice.lhs | 9 +- compiler/typecheck/TcTyClsDecls.lhs | 58 +++--- compiler/utils/UniqSet.lhs | 3 + 8 files changed, 254 insertions(+), 246 deletions(-) }}} -- Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7916#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#7916: PolyKinds without type signatures ----------------------------------------+----------------------------------- Reporter: monoidal | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.7 Resolution: fixed | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC rejects valid program | Difficulty: Unknown Testcase: polykinds/T7916 | Blockedby: Blocking: | Related: ----------------------------------------+----------------------------------- Changes (by simonpj): * status: new => closed * testcase: => polykinds/T7916 * resolution: => fixed Comment: This patch is important too: {{{ commit 09b025eabf08044b67d047b970cd99add97e9d77 Author: Simon Peyton Jones <simonpj@microsoft.com> Date: Wed May 22 17:43:56 2013 +0100 Wibbles to yesterday's "Simplify kind generalisation" patch In particular, in mkExport we must quantify over the kind variables mentioned in the kinds of the free type variables }}} -- Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7916#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#7916: PolyKinds without type signatures ----------------------------------------+----------------------------------- Reporter: monoidal | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.7 Resolution: fixed | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC rejects valid program | Difficulty: Unknown Testcase: polykinds/T7916 | Blockedby: Blocking: | Related: ----------------------------------------+----------------------------------- Comment(by simonpj): Thank you for such a nice well characterised bug report. Simon -- Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7916#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#7916: PolyKinds without type signatures ----------------------------------------+----------------------------------- Reporter: monoidal | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.7 Resolution: fixed | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC rejects valid program | Difficulty: Unknown Testcase: polykinds/T7916 | Blockedby: Blocking: | Related: ----------------------------------------+----------------------------------- Comment(by monoidal): Thank you for fixing it! I appreciate it. Maybe I'm doing something wrong, but the regression test does not seem to capture the bug - it compiles before and after the fix. Here's one possibility to test that g is really polymorphic: {{{ {-# LANGUAGE PolyKinds, ExplicitForAll #-} module T7916 where f :: forall (m :: k -> *) (a :: k). m a -> m a f = id g = f data M f = M (f Int) -- Test that g :: forall (m :: k -> *) (a :: k). m a -> m a g1 = g :: [Int] -> [Int] g2 = g :: M [] -> M [] }}} Both g1 and g2 are needed to detect the behaviour before the fix. -- Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7916#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#7916: PolyKinds without type signatures ----------------------------------------+----------------------------------- Reporter: monoidal | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.7 Resolution: fixed | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC rejects valid program | Difficulty: Unknown Testcase: polykinds/T7916 | Blockedby: Blocking: | Related: ----------------------------------------+----------------------------------- Comment(by simonpj): Absolutely right. I've pushed a patch with your change. Thanks. Simon -- Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7916#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC