[GHC] #14288: ScopedTypeVariables with nexted foralls broken since 8.0.2
#14288: ScopedTypeVariables with nexted foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: | Owner: (none) MikolajKonarski | Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 (Type checker) | Keywords: | Operating System: Linux Architecture: x86_64 | Type of failure: GHC rejects (amd64) | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The following example fails in 8.2.1 and 8.0.2. Works fine in 7.10.3. If that's intended (that only the first forall has extended scope), I didn't find any mention of that in GHC manual. The two commented out variants work fine in all. {{{#!hs {-# LANGUAGE ScopedTypeVariables #-} main :: IO () main = do -- let f :: forall a ref. ref () -> () -- let f :: forall ref. forall a. ref () -> () let f :: forall a. forall ref. ref () -> () f x = let r :: ref () r = x in () return $ f (Just ()) }}} The error (the same in 8.2.1 and 8.0.2) is: {{{#!hs $ ghc --make forall.hs [1 of 1] Compiling Main ( forall.hs, forall.o ) forall.hs:8:21: error: • Couldn't match type ‘ref’ with ‘ref1’ ‘ref’ is a rigid type variable bound by the type signature for: f :: forall a (ref :: * -> *). ref () -> () at forall.hs:6:29 ‘ref1’ is a rigid type variable bound by the type signature for: r :: forall (ref1 :: * -> *). ref1 () at forall.hs:7:22 Expected type: ref1 () Actual type: ref () • In the expression: x In an equation for ‘r’: r = x In the expression: let r :: ref () r = x in () • Relevant bindings include r :: ref1 () (bound at forall.hs:8:17) x :: ref () (bound at forall.hs:7:9) f :: ref () -> () (bound at forall.hs:7:7) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by adamgundry): * cc: adamgundry (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I believe this is by design. But I agree that the manual does not mention it. Simon, I think this was a part of the big refactoring around `HsImplicitBndrs` and `HsSigType`s and such. Do you agree? Regardless, we should update the manual. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): For what it's worth, it's quite simple to change the behavior to make it work the way you desire: {{{#!diff diff --git a/compiler/hsSyn/HsTypes.hs b/compiler/hsSyn/HsTypes.hs index b9cd946..5e0f885 100644 --- a/compiler/hsSyn/HsTypes.hs +++ b/compiler/hsSyn/HsTypes.hs @@ -54,7 +54,8 @@ module HsTypes ( hsScopedTvs, hsWcScopedTvs, dropWildCards, hsTyVarName, hsAllLTyVarNames, hsLTyVarLocNames, hsLTyVarName, hsLTyVarLocName, hsExplicitLTyVarNames, - splitLHsInstDeclTy, getLHsInstDeclHead, getLHsInstDeclClass_maybe, + splitLHsInstDeclTy, splitNestedLHsSigmaTys, + getLHsInstDeclHead, getLHsInstDeclClass_maybe, splitLHsPatSynTy, splitLHsForAllTy, splitLHsQualTy, splitLHsSigmaTy, splitHsFunType, splitHsAppsTy, @@ -76,7 +77,7 @@ import PlaceHolder ( PlaceHolder(..) ) import HsExtension import Id ( Id ) -import Name( Name ) +import Name( Name, NamedThing(..) ) import RdrName ( RdrName ) import NameSet ( NameSet, emptyNameSet ) import DataCon( HsSrcBang(..), HsImplBang(..), @@ -843,17 +844,19 @@ hsWcScopedTvs sig_ty | HsWC { hswc_wcs = nwcs, hswc_body = sig_ty1 } <- sig_ty , HsIB { hsib_vars = vars, hsib_body = sig_ty2 } <- sig_ty1 = case sig_ty2 of - L _ (HsForAllTy { hst_bndrs = tvs }) -> vars ++ nwcs ++ - map hsLTyVarName tvs + fa_ty@(L _ (HsForAllTy {})) + | (tvs, _, _) <- splitNestedLHsSigmaTys fa_ty + -> vars ++ nwcs ++ map hsLTyVarName tvs -- include kind variables only if the type is headed by forall -- (this is consistent with GHC 7 behaviour) - _ -> nwcs + _ -> nwcs hsScopedTvs :: LHsSigType GhcRn -> [Name] -- Same as hsWcScopedTvs, but for a LHsSigType hsScopedTvs sig_ty | HsIB { hsib_vars = vars, hsib_body = sig_ty2 } <- sig_ty - , L _ (HsForAllTy { hst_bndrs = tvs }) <- sig_ty2 + , fa_ty@(L _ (HsForAllTy {})) <- sig_ty2 + , (tvs, _, _) <- splitNestedLHsSigmaTys fa_ty = vars ++ map hsLTyVarName tvs | otherwise = [] @@ -953,9 +956,10 @@ mkHsAppTys = foldl mkHsAppTy -- splitHsFunType decomposes a type (t1 -> t2 ... -> tn) -- Breaks up any parens in the result type: -- splitHsFunType (a -> (b -> c)) = ([a,b], c) --- Also deals with (->) t1 t2; that is why it only works on LHsType Name +-- Also deals with (->) t1 t2; that is why it only works on NamedThings. -- (see Trac #9096) -splitHsFunType :: LHsType GhcRn -> ([LHsType GhcRn], LHsType GhcRn) +splitHsFunType :: NamedThing (IdP pass) + => LHsType pass -> ([LHsType pass], LHsType pass) splitHsFunType (L _ (HsParTy ty)) = splitHsFunType ty @@ -966,7 +970,7 @@ splitHsFunType (L _ (HsFunTy x y)) splitHsFunType orig_ty@(L _ (HsAppTy t1 t2)) = go t1 [t2] where -- Look for (->) t1 t2, possibly with parenthesisation - go (L _ (HsTyVar _ (L _ fn))) tys | fn == funTyConName + go (L _ (HsTyVar _ (L _ fn))) tys | getName fn == funTyConName , [t1,t2] <- tys , (args, res) <- splitHsFunType t2 = (t1:args, res) @@ -1044,6 +1048,7 @@ splitLHsPatSynTy ty = (univs, reqs, exis, provs, ty4) (exis, ty3) = splitLHsForAllTy ty2 (provs, ty4) = splitLHsQualTy ty3 +-- | Split a sigma type into its parts. splitLHsSigmaTy :: LHsType pass -> ([LHsTyVarBndr pass], LHsContext pass, LHsType pass) splitLHsSigmaTy ty @@ -1051,6 +1056,50 @@ splitLHsSigmaTy ty , (ctxt, ty2) <- splitLHsQualTy ty1 = (tvs, ctxt, ty2) +-- | Split a sigma type into its parts, going underneath as many 'HsForAllTy's +-- and 'HsQualTy's as possible. +-- +-- 'splitNestedLHsSigmaTys' is to 'splitLHsSigmaTy' as 'tcSplitNestedSigmaTys' +-- is to 'tcSplitSigmaTy' (from "TcType"). +splitNestedLHsSigmaTys + :: NamedThing (IdP pass) + => LHsType pass + -> ([LHsTyVarBndr pass], LHsContext pass, LHsType pass) +splitNestedLHsSigmaTys ty + -- If there's a forall or context, split it apart and try splitting the + -- rho type underneath it. + | Just (arg_tys, tvs1, L src1 theta1, rho1) <- deepSplitLHsSigmaTy_maybe ty + = let (tvs2, L src2 theta2, rho2) = splitNestedLHsSigmaTys rho1 + in ( tvs1 ++ tvs2, L (combineSrcSpans src1 src2) (theta1 ++ theta2) + , nlHsFunTys arg_tys rho2 ) + -- If there's no forall or context, we're done. + | otherwise = ([], L noSrcSpan [], ty) + where + -- These really should be imported from HsUtils, but that would lead + -- to import cycles. + nlHsFunTy :: LHsType name -> LHsType name -> LHsType name + nlHsFunTy a b = noLoc (HsFunTy a b) + + nlHsFunTys :: [LHsType name] -> LHsType name -> LHsType name + nlHsFunTys args res = foldr nlHsFunTy res args + +deepSplitLHsSigmaTy_maybe + :: NamedThing (IdP pass) + => LHsType pass + -> Maybe ( [LHsType pass], [LHsTyVarBndr pass], LHsContext pass + , LHsType pass ) +deepSplitLHsSigmaTy_maybe ty + | (arg_tys1, res_ty) <- splitHsFunType ty + , not (null arg_tys1) -- If not, splitHsFunType didn't find any arrow types + , Just (arg_tys2, tvs, theta, rho) <- deepSplitLHsSigmaTy_maybe res_ty + = Just (arg_tys1 ++ arg_tys2, tvs, theta, rho) + + | (tvs, hs_theta@(L _ theta), rho) <- splitLHsSigmaTy ty + , not (null tvs && null theta) + = Just ([], tvs, hs_theta, rho) + + | otherwise = Nothing + splitLHsForAllTy :: LHsType pass -> ([LHsTyVarBndr pass], LHsType pass) splitLHsForAllTy (L _ (HsForAllTy { hst_bndrs = tvs, hst_body = body })) = (tvs, body) splitLHsForAllTy body = ([], body) }}} Applying this patch makes that test case compile successfully. The only question is if we //should// apply the patch at all. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by MikolajKonarski): In this rare case I have no preference. I assumed this is a bug, because it suddenly changed in 8.0.2. The current version indeed makes sense, e.g., if one wants different variables to be scoped differently. Are we sure that anything one can write with many foralls can be written with one forall? No edge cases with line-breaks, kinds, etc.? If so, perhaps that's a good thing to write in the manual as well. Thank you for the feedback and for the patch. You, guys, rock. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Richard and I both think we should stick with the current behaviour, and specify it in the user manual. That is, with `-XScopedTypeVariables`, and a signature {{{ f :: forall a b c. blah <definition of f> }}} then `a`, `b` and `c` scope over f's definition, but no other type variables do. This applies unconditionally, even if `blah` starts with another `forall`. The `forall` must appear literally, not hidden by a type synonym. Eg. no variables scope here {{{ type Foo = forall a b. a -> b -> Int f :: Foo f = e -- a and b are not in scope here }}} This rule is simple, and does not restrict expressiveness. Otherwise we land up trying to decide where to draw the line (and having to explain where it is drawn, in the user manual). Eg {{{ f :: forall a. forall b. blah f :: forall a. a -> forall b. blah f :: forall a. Eq a => forall b. blah }}} Would someone care to update the user manual? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I'm worried that this design decision will come back to bite us once the [https://github.com/ghc-proposals/ghc- proposals/blob/dbf516088d2839432c9568c3d1f7ae28d46aeb43/proposals/0005 -bidir-constr-sigs.rst pattern synonym construction function signatures] proposal is implemented. To recap, if you have an explicitly bidirectional pattern synonym like: {{{#!hs data T a where MkT :: forall a b. (Show b) => a -> b -> T a pattern ExNumPat :: forall a. (Num a, Eq a) => forall b. (Show b) => b -> T a pattern ExNumPat x <- MkT 42 x where ExNumPat x = MkT 42 x }}} Then this proposal would allow you to write an explicit type signature for the builder expression, like so: {{{#!hs pattern ExNumPat :: forall a. (Num a, Eq a) => forall b. (Show b) => b -> T a pattern ExNumPat x <- MkT 42 x where ExNumPat :: forall a. (Num a, Ord a) => forall b. (Show b) => b -> T a ExNumPat x = MkT 42 x }}} Where this type signature must be the same as the pattern signature save for the required constraints, which are allowed to be different. Once we gain the ability to write type signatures for builder expressions like this (and thus, the ability to lexically scope type variables with `-XScopedTypeVariables`), folks will naturally want to write builders with `-XTypeApplications` like this: {{{#!hs ExNumPat :: forall a. (Num a, Ord a) => forall b. (Show b) => b -> T a ExNumPat x = MkT @a @b 42 x }}} (This is a relatively simple example, but you could imagine this being more useful when fancier types are involved.) But there's a big problem here—. By the rules of `-XScopedTypeVariables`, only `a` will be in scope in the builder's RHS, not `b`! With normal function type signatures, you can work around this problem by just smashing `forall a. forall b` into `forall a b`, but with pattern synonyms, we cannot do this—the required type variables and the provided type variables //must// be quantified separately! So this design prevents us from writing pattern synonym builders that visibly apply provided type variables using `-XTypeApplications`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): As far as specifying how GHC should bring variables from nested `forall`s into scope, I don't think it's nearly as difficult as you're making it out to be. The algorithm would be as follows: when `ScopedTypeVariables` is enabled and an identifier with an explicit type signature `T` is being typechecked, then the set of variables `foralls(T)` is brought into scope, where: * `foralls(forall a_1 ... a_k. T) = {a_1, ..., a_k} ∪ foralls (T)` * `foralls(C => T) = foralls(T)` * `foralls(b -> c) = foralls(c)` Note that this doesn't expand type synonyms, so we needn't worry about your `Foo` example in comment:5 bringing variables into scope. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): What do you think of {{{#!hs f :: forall a. a -> Int -> forall b. (a, b) f x = const (x, undefined :: b) }}} Note that the quantifier for `b` hasn't been encountered in the term definition, which takes only one argument. Accepting this would be strange, indeed, in my view. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I don't see what is strange about this? It's no stranger than `f :: forall a b. a -> Int -> (a, b)` at least, which is accepted. Replying to [comment:8 goldfire]:
Note that the quantifier for `b` hasn't been encountered in the term definition, which takes only one argument.
Yeah... and? I don't see what the term definition has to do with anything here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): FWIW I don't have a very strong opinion here. I'd like to know what others think. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Actually, the issue I mentioned about pattern synonyms applies //today//. That it, this typechecks: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} data T a where MkT :: forall a b. (Show b) => a -> b -> T a pattern ExNumPat :: forall a. (Num a, Eq a) => forall b. (Show b) => b -> T a pattern ExNumPat x <- MkT 42 x where ExNumPat x = MkT @a 42 x }}} But this (with `@b`) doesn't! {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} data T a where MkT :: forall a b. (Show b) => a -> b -> T a pattern ExNumPat :: forall a. (Num a, Eq a) => forall b. (Show b) => b -> T a pattern ExNumPat x <- MkT 42 x where ExNumPat x = MkT @a @b 42 x }}} Moreover, there's no workaround for this, since one can't combine the two `forall`s in the pattern signature for the reasons discussed in comment:6. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Yes, that's pretty convincing. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): That being said, I'm sympathetic to the desire to have a consistent, predictable way to determine when exactly a `forall`'d variable from a type signature is brought into scope, so I don't want to hammer too hard on this point unless goldfire is on board too. I'm sure goldfire has a convincing example in comment:8, but I'm having trouble understanding what makes it convincing. I'm grasping at straws here, but is the concern that something like this (with invisible patterns written out explicitly) should "intuitively" typecheck: {{{#!hs f1 :: forall a. a -> Int -> forall b. (a, b) f1 @a x i @b = const (x, undefined :: b) i }}} But in the eta-reduced version: {{{#!hs f2 :: forall a. a -> Int -> forall b. (a, b) f2 @a x = const (x, undefined :: b {-?-}) }}} `b` isn't bound by an invisible pattern? Or is there some other reason why this should be considered "strange"? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): comment:13 has it. That's why it's strange. When I program in Haskell, I implicitly believe I'm programming in something quite like F_omega, but the compiler puts in gobs of annotations. And I find it disturbing and strange when the compiler rearranges my expressions. Also, what happens when you replace the right-hand side of the expression with `undefined`? Consider {{{#!hs f3 :: forall a b. a -> Int -> (a, b) f3 x = undefined f4 :: forall a. a -> Int -> forall b. (a, b) f4 x = undefined }}} Evaluating {{{f3 True `seq` ()}}} diverges, while {{{f4 True `seq` ()}}} returns `()`. This is because `f4 True` is really a lambda, due to the parameter-swizzling. I argue once we have a proper story for visible type patterns, `f4 True` will also be able to diverge, and then my original example becomes ever stranger. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): OK. I tried out a similar example in Idris to see how it handles an example like `f4` from comment:14, and it turns out that Idris rejects it as well. So I'm now convinced that we shouldn't attempt to support examples like that. In light of this, what if we changed `foralls` from comment:7 to just this? * `foralls(forall a_1 ... a_k. T) = {a_1, ..., a_k} ∪ foralls (T)` * `foralls(C => T) = foralls(T)` That is, simply remove the `foralls(b -> c) = foralls(c)` case. This means that of these examples from comment:5: {{{#!hs f1 :: forall a. forall b. blah f2 :: forall a. a -> forall b. blah f3 :: forall a. Eq a => forall b. blah }}} Then in `f1` and `f3`, `a` and `b` will be lexically scoped, but in `f2`, only `a` will be lexically scoped. Does that sound agreeable? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Good with me. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: RyanGlScott Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * owner: (none) => RyanGlScott * milestone: => 8.4.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: RyanGlScott Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Hm. Implementing the renaming part of this patch is a breeze, but modifying the typechecker is proving to be a pain. The source of my headaches can be traced down to this [http://git.haskell.org/ghc.git/blob/0e9681268a38cbc15c9c2b50979624732c9077ce... tcInstType] function: {{{#!hs tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar])) -- ^ How to instantiate the type variables -> Id -- ^ Type to instantiate -> TcM ([(Name, TcTyVar)], TcThetaType, TcType) -- ^ Result -- (type vars, preds (incl equalities), rho) }}} The problem is that at the moment, the first part of the triple that `tcInstType` returns corresponds to the lexically scoped type variables. But there's an assumption that these variables will all appear consecutively, uninterrupted by a `TcThetaType`. With the proposed changes in this ticket, this assumption will no longer hold true. But I can't just return more type variables in the first part of the triple, because almost all call sites of `tcInstType` reconstruct the instantiated type with something like `forall <tvs>. <theta-type> => <tc- type>`. In other words, cramming more type variables would cause the wrong types to be constructed! So `tcInstType` just seems to be designed the wrong way for what I want to accomplish, but I can't figure out how to redesign it sensibly... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: RyanGlScott Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Yes, this is awkward. When we instantiate a type signature, we currently instantiate only the outer foralls and context. See `TcSigs.tcInstSig`. The scoped type variables come from the `sig_inst_skols`. Very similar story in `TcBinds.tcPolyCheck`. I suppose we can generalise this story. Instead of having {{{ data TcIdSigInst = TISI { ... , sig_inst_skols :: [(Name, TcTyVar)] , sig_inst_theta :: TcThetaType ... } }}} I suppose we could have a list of pairs of those things: {{{ data TcIdSigInst = TISI { ... , sig_inst_prefis :: [([(Name, TcTyVar)], TcThetaType)] ... } }}} Or maybe, more uniformly: {{{ data TcIdSigInst = TISI { ... , sig_inst_prefis :: [SigInstSpec] ... } data SigInstSpec = SITyVar Name TcTyVar | SIPred TcPredType }}} Then `tcInstType` might have type {{{ tcInstType :: (...) -> Id -> TcM ([SigInstSpec], TcRhoType) }}} I think we could carry this through uniformly. But I haven't tried. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: RyanGlScott Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: #14498 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #14498 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: RyanGlScott Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: #14498 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: RyanGlScott Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: #14498 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I had been pushing for this change since I was convinced it was necessary to bring into scope the existentially quantified type variables in pattern synonym type signatures. But the discussion in #14498 has marched in the opposite direction (in particular, see https://ghc.haskell.org/trac/ghc/ticket/14498#comment:16). There, the consensus seems to be that we should //not// bring into scope these existentially quantified variables. In light of this, my original motivation for pursuing this ticket has disappeared, so I think we should go with the plan in comment:5 and document the current behavior. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: RyanGlScott Type: bug | Status: patch Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: #14498 | Differential Rev(s): Phab:D4272 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D4272 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2
-------------------------------------+-------------------------------------
Reporter: MikolajKonarski | Owner: RyanGlScott
Type: bug | Status: patch
Priority: normal | Milestone: 8.4.1
Component: Compiler (Type | Version: 8.2.1
checker) |
Resolution: | Keywords:
Operating System: Linux | Architecture: x86_64
Type of failure: GHC rejects | (amd64)
valid program | Test Case:
Blocked By: | Blocking:
Related Tickets: #14498 | Differential Rev(s): Phab:D4272
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ryan Scott
#14288: ScopedTypeVariables with nested foralls broken since 8.0.2 -------------------------------------+------------------------------------- Reporter: MikolajKonarski | Owner: RyanGlScott Type: bug | Status: closed Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: fixed | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: #14498 | Differential Rev(s): Phab:D4272 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: patch => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14288#comment:25 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC