#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