[GHC] #15954: LiberalTypeSynonyms unsaturation check doesn't kick in
#15954: LiberalTypeSynonyms unsaturation check doesn't kick in -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC accepts Unknown/Multiple | invalid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- GHC accepts this program: {{{#!hs {-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} module Bug where import GHC.Exts (Any) type KindOf (a :: k) = k type A a = (Any :: a) type KA = KindOf A }}} But it really oughtn't to. After all, we have an unsaturated use of `A` in `KindOf A`, and we don't have `LiberalTypeSynonyms` enabled! What's even stranger is that there seems to be something about this exact setup that sneaks by `LiberalTypeSynonyms`' validity checks. If I add another argument to `A`: {{{#!hs type A x a = (Any :: a) }}} Then it //does// error: {{{ $ /opt/ghc/8.6.2/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:10:1: error: • Illegal polymorphic type: forall a -> a Perhaps you intended to use LiberalTypeSynonyms • In the type synonym declaration for ‘KA’ | 10 | type KA = KindOf A | ^^^^^^^^^^^^^^^^^^ }}} Similarly, if I use something besides `KindOf`: {{{#!hs {-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} module Bug where import GHC.Exts (Any) type A a = (Any :: a) type B a = Int type C = B A }}} Then I also get the same `Illegal polymorphic type: forall a -> a` error. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15954 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15954: LiberalTypeSynonyms unsaturation check doesn't kick in -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler (Type | Version: 8.6.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Here is another example which doesn't require `ImpredicativeTypes`, `PolyKinds`, or visible dependent quantification: {{{#!hs {-# LANGUAGE KindSignatures #-} {-# LANGUAGE RankNTypes #-} module Bug where import Data.Kind type A a = Int type B (a :: Type -> Type) = forall x. x -> x type C = B A }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15954#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15954: LiberalTypeSynonyms unsaturation check doesn't kick in -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler (Type | Version: 8.6.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): The culprit appears to be the [http://git.haskell.org/ghc.git/blob/984b75de7082689ebcc6e9d17b37f2c9b3702f71... first case] of `check_type`: {{{#!hs check_type env ctxt rank ty | not (null tvbs && null theta) = do { traceTc "check_type" (ppr ty $$ ppr (forAllAllowed rank)) ; checkTcM (forAllAllowed rank) (forAllTyErr env rank ty) -- Reject e.g. (Maybe (?x::Int => Int)), -- with a decent error message ; check_valid_theta env' SigmaCtxt theta -- Allow type T = ?x::Int => Int -> Int -- but not type T = ?x::Int ; check_type env' ctxt rank tau -- Allow foralls to right of arrow ; checkTcM (not (any (`elemVarSet` tyCoVarsOfType phi_kind) tvs)) (forAllEscapeErr env' ty tau_kind) } where (tvbs, phi) = tcSplitForAllVarBndrs ty (theta, tau) = tcSplitPhiTy phi tvs = binderVars tvbs (env', _) = tidyVarBndrs env tvs tau_kind = typeKind tau phi_kind | null theta = tau_kind | otherwise = liftedTypeKind -- If there are any constraints, the kind is *. (#11405) }}} In particular, this function uses `tcSplitForAllVarBndrs` and `tcSplitPhiTy` to decompose the right-hand side of a type synonym. What happens when that right-hand side is `B A` (from comment:1)? Well, as it happens, both `tcSplitForAllVarBndrs` and `tcSplitPhiTy` //expand type synonyms//, so `check_type` actually checks `forall x. x -> x` for validity, not `B A`! In other words, GHC is completely oblivious to the fact that `A` is unsaturated, since it's not checking the type `B A` in the first place. I suppose the prudent thing to do here would be to conjure up variations of `tcSplitForAllVarBndrs` and `tcSplitPhiTy` that don't expand type synonyms? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15954#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15954: LiberalTypeSynonyms unsaturation check doesn't kick in -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler (Type | Version: 8.6.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
I suppose the prudent thing to do here would be to conjure up variations of tcSplitForAllVarBndrs and tcSplitPhiTy that don't expand type synonyms?
Actually I think it would suffice simply to put this `check_type` equation (the one you cite in comment:2) last, after the one for `TyConApp`. The latter does the right thing for synonyms, and expands them. Oh, the `FunTy` case should still follow the moved equation; consider `t1 => t2`. Would you like to try that? Thanks! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15954#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15954: LiberalTypeSynonyms unsaturation check doesn't kick in -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler (Type | Version: 8.6.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Thanks, I've implemented your suggestion. There are three error message regressions as a result, so I'd like your feedback on them. 1. In `T15859`: {{{#!diff diff -uw "dependent/should_fail/T15859.run/T15859.stderr.normalised" "dependent/should_fail/T15859.run/T15859.comp.stderr.normalised" --- dependent/should_fail/T15859.run/T15859.stderr.normalised 2018-11-27 06:38:24.627899584 -0500 +++ dependent/should_fail/T15859.run/T15859.comp.stderr.normalised 2018-11-27 06:38:24.635899818 -0500 @@ -1,6 +1,7 @@ -T15859.hs:13:5: - Cannot apply expression of type ‘forall k -> k -> *’ - to a visible type argument ‘Int’ +T15859.hs:13:19: + Illegal polymorphic type: forall k -> k -> * + Perhaps you intended to use LiberalTypeSynonyms + In an expression type signature: KindOf A + In the expression: undefined :: KindOf A In the expression: (undefined :: KindOf A) @Int - In an equation for ‘a’: a = (undefined :: KindOf A) @Int }}} This one doesn't bother me much, since that code really ought to have been enabling `LiberalTypeSynonyms` in the first place (indeed, investigating that code is what led me to discovering this bug). I think I'll fix this by just enabling `LiberalTypeSynonyms` in the test case. 2. In `T7809`: {{{#!diff diff -uw "typecheck/should_fail/T7809.run/T7809.stderr.normalised" "typecheck/should_fail/T7809.run/T7809.comp.stderr.normalised" --- typecheck/should_fail/T7809.run/T7809.stderr.normalised 2018-11-27 06:42:45.604510107 -0500 +++ typecheck/should_fail/T7809.run/T7809.comp.stderr.normalised 2018-11-27 06:42:45.615510428 -0500 @@ -1,6 +1,5 @@ T7809.hs:8:8: - Illegal polymorphic type: PolyId + Illegal polymorphic type: forall a. a -> a GHC doesn't yet support impredicative polymorphism - In the type signature: - foo :: F PolyId + In the type signature: foo :: F PolyId }}} This one is a bit concerning, since we've regressed from a nice error message about `PolyId` (which is what the user wrote) to instead mentioning `forall a. a -> a` (which requires the user to perform some detective work to figure out where it comes from). I haven't figured out yet why this happens (indeed, I'm surprised to see a type synonym being expanded //more// after this change). 3. In `tc149`: {{{ Compile failed (exit code 1) errors were: tc149.hs:8:8: error: • The type synonym ‘Id’ should have 1 argument, but has been given none • In the type signature: foo :: Generic Id Id }}} This is the most concerning one, since `tc149` is actually expected to //typecheck//! For the sake of reference, here is the source code for this test case: {{{#!hs {-# LANGUAGE RankNTypes #-} module ShouldCompile where type Generic i o = forall x. i x -> o x type Id x = x foo :: Generic Id Id foo = error "urk" -- The point here is that we instantiate "i" and "o" -- with a partially applied type synonym. This is -- OK in GHC because we check type validity only *after* -- expanding type synonyms. -- -- However, a bug in GHC 5.03-Feb02 made this break a -- type invariant (see Type.mkAppTy) }}} Mysteriously, that comment claims that this code ought to typecheck as- is. But shouldn't that only be the case if `LiberalTypeSynonyms` is enabled? This test case was added all the way back in 2002 (in commit ddb3ea2220621d9393ebb08ce3548ac2118a57c2) without much exposition, so it's difficult for me to tell whether this test case is legitimate or not. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15954#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15954: LiberalTypeSynonyms unsaturation check doesn't kick in -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler (Type | Version: 8.6.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * Attachment "T15954.patch" added. Giving up on this for now until simonpj responds. Until then, I'll stash my WIP patch here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15954 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15954: LiberalTypeSynonyms unsaturation check doesn't kick in -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler (Type | Version: 8.6.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Sorry to be slow. 1. Yes, this is a good message 2. I'm not so bothered here. Is it really better to say `Illegal polymorphic type: PolyId`? It doesn't look polymorphic. (In (1) would you have preferred `Illegal polymorphic type A`? That doesn't look polymorphic either. Also if we had {{{ type A = (forall a. a->a) -> Int foo :: F A foo = ... }}} we couldn't possibly report in terms of `A`. It's easy to see why it happens: we've moved synonym expansion first! 3. `tc149`. Yes I agree, it should have `Language LiberalTypeSynonyms` at the top. I think the test predates the flag. This change fixes an outright bug; and I think the regression is arguably and improvement. So let's do it! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15954#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15954: LiberalTypeSynonyms unsaturation check doesn't kick in -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.6.3 Component: Compiler (Type | Version: 8.6.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5402 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D5402 Comment: Alright. If you're happy with the new output, then I am too. Phab:D5402 implements this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15954#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15954: LiberalTypeSynonyms unsaturation check doesn't kick in -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.6.3 Component: Compiler (Type | Version: 8.6.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5402 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): PS. Here's an idea. In `check_syn_tc_app`, you could wrap the recursive call to `check_type` in `addErrCtxt "In the expansion of type synonym <blah>`. That would give us the best of both worlds, including for the trickier case I described in comment:5 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15954#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15954: LiberalTypeSynonyms unsaturation check doesn't kick in -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.6.3 Component: Compiler (Type | Version: 8.6.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5402 Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Done. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15954#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15954: LiberalTypeSynonyms unsaturation check doesn't kick in
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: patch
Priority: normal | Milestone: 8.6.3
Component: Compiler (Type | Version: 8.6.2
checker) |
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
Type of failure: GHC accepts | Unknown/Multiple
invalid program | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s): Phab:D5402
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ryan Scott
#15954: LiberalTypeSynonyms unsaturation check doesn't kick in -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.6.2 checker) | Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC accepts | Test Case: invalid program | typecheck/should_fail/T15954 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5402 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: patch => closed * testcase: => typecheck/should_fail/T15954 * resolution: => fixed * milestone: 8.6.3 => 8.8.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15954#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC