[GHC] #16140: Cannot create type synonym for quantified constraint without ImpredicativeTypes
GHC
ghc-devs at haskell.org
Thu Jan 17 00:56:28 UTC 2019
#16140: Cannot create type synonym for quantified constraint without
ImpredicativeTypes
-------------------------------------+-------------------------------------
Reporter: Ashley Yakeley | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.6.3
Resolution: | Keywords:
| QuantifiedConstraints,
| ImpredicativeTypes
Operating System: Unknown/Multiple | Architecture:
Type of failure: GHC rejects | Unknown/Multiple
valid program | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by RyanGlScott):
Thanks for the very detailed advice. After implementing the plan in
comment:12, the original program in this ticket is now accepted. But we're
not out of the woods yet, since several test cases now topple over. I'll
try to summarize the issues below:
* Certain programs no longer need `QuantifiedConstraints` to typecheck,
even though they should. For instance, this typechecks:
{{{#!hs
{-# LANGUAGE RankNTypes #-}
module Bug where
f :: (forall a. Eq a) => Int
f = 42
}}}
Likely reason: the place where we check if `QuantifiedConstraints` is
enabled (`checkTcM (forAllAllowed rank)` in `check_type`) is no longer
reachable from `check_pred_ty`, since it no longer invokes `check_type`.
Similarly, it's now possible to sneak impredicativity into constraints,
as the following program is now accepted, even though it shouldn't be:
{{{#!hs
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
module Bug where
f :: Num (forall a. a) => Int
f = 42
}}}
* `TypeApplications` now require language extensions that they didn't
before. For instance, the `T12447` test case used to be work:
{{{
ghci> :set -XRankNTypes -XConstraintKinds -XTypeApplications
ghci> deferEither @(_ ~ _)
}}}
Now, it produces the following error:
{{{
+
+<interactive>:1:1:
+ Illegal equational constraint _0 ~ _1
+ (Use GADTs or TypeFamilies to permit this)
+ In the expression: deferEither @(_ ~ _)
*** unexpected failure for T12447(ghci)
}}}
Depending on one's perspective, this might be a desirable outcome. But
it is a break from convention, so it's worth noting.
Another example from the `TypeRep` test case:
{{{
Compile failed (exit code 1) errors were:
[1 of 1] Compiling Main ( TypeRep.hs, TypeRep.o )
TypeRep.hs:41:11: error:
• Non type-variable argument in the constraint: Eq Int
(Use FlexibleContexts to permit this)
• In the second argument of ‘($)’, namely
‘rep @((Eq Int, Eq String) :: Constraint)’
In a stmt of a 'do' block:
print $ rep @((Eq Int, Eq String) :: Constraint)
In the expression:
do print $ rep @String
print $ rep @Char
print $ rep @Int
print $ rep @Word
....
*** unexpected failure for TypeRep(normal)
}}}
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16140#comment:13>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list