Impredicativity checking is fooled by a type synonym
Consider the following functions, which all instantiate undefined
impredicatively:
{-# LANGUAGE RankNTypes #-}
module Bug where
a :: (forall a. a) -> ()
a = undefined
b :: (Show a => a) -> ()
b = undefined
type C = forall a. a
c :: C -> ()
c = undefined
type D a = Show a => a
d :: D a -> ()
d = undefined
a
, b
, and c
will each fail to typecheck:
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:5:5: error:
• Cannot instantiate unification variable ‘a1’
with a type involving polytypes: (forall a. a) -> ()
GHC doesn't yet support impredicative polymorphism
• In the expression: undefined
In an equation for ‘a’: a = undefined
|
5 | a = undefined
| ^^^^^^^^^
Bug.hs:8:5: error:
• Cannot instantiate unification variable ‘a2’
with a type involving polytypes: (Show a => a) -> ()
GHC doesn't yet support impredicative polymorphism
• In the expression: undefined
In an equation for ‘b’: b = undefined
• Relevant bindings include
b :: (Show a => a) -> () (bound at Bug.hs:8:1)
|
8 | b = undefined
| ^^^^^^^^^
Bug.hs:12:5: error:
• Cannot instantiate unification variable ‘a0’
with a type involving polytypes: C -> ()
GHC doesn't yet support impredicative polymorphism
• In the expression: undefined
In an equation for ‘c’: c = undefined
|
12 | c = undefined
| ^^^^^^^^^
Curiously, there is no error message for d
. In fact, if you comment out a
, b
, and c
, then d
will typecheck! This is concerning, as d
is just a variant of b
with an extra type synonym thrown into the mix.
Why is it that c
, which also uses a type synonym, is rejected, but d
is accepted? It's ultimately because of GHC.Tc.Utils.Unify.preCheck
, which powers GHC's impredicative instantiation checks. This part of preCheck
is suspicious:
preCheck dflags ty_fam_ok tv ty
= fast_check ty
where
...
fast_check :: TcType -> MetaTyVarUpdateResult ()
...
fast_check (TyConApp tc tys)
| bad_tc tc = MTVU_Bad
| otherwise = mapM fast_check tys >> ok
...
bad_tc :: TyCon -> Bool
bad_tc tc
| not (impredicative_ok || isTauTyCon tc) = True
| not (ty_fam_ok || isFamFreeTyCon tc) = True
| otherwise = False
If bad_tc
returns True
, then that results in a TyConApp
being flagged as impredicative. bad_tc
first checks if impredicative_ok
is True
(i.e., if ImpredicativeTypes
is enabled), and since that isn't the case in the program above, it checks isTauTyCon tc
. For type synonyms like C
and D
, this checks if the RHS of the type synonym is a tau type, as defined by the isTauTy
function:
-- @isTauTy@ tests if a type has no foralls
isTauTy :: Type -> Bool
isTauTy ty | Just ty' <- coreView ty = isTauTy ty'
isTauTy (TyVarTy _) = True
isTauTy (LitTy {}) = True
isTauTy (TyConApp tc tys) = all isTauTy tys && isTauTyCon tc
isTauTy (AppTy a b) = isTauTy a && isTauTy b
isTauTy (FunTy _ a b) = isTauTy a && isTauTy b
isTauTy (ForAllTy {}) = False
isTauTy (CastTy ty _) = isTauTy ty
isTauTy (CoercionTy _) = False -- Not sure about this
However, isTauTy
only checks if a type contains forall
s, not contexts! As a result, C
is flagged as impredicative, but D a
is not.
I wonder if the definition of isTauTy
should be expanded to detect higher-rank contexts in addition to higher-rank forall
s? In other words, should the following change be applied?
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 1e7af2d8cf..3cf4231480 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -1864,6 +1864,7 @@ isTauTy (TyVarTy _) = True
isTauTy (LitTy {}) = True
isTauTy (TyConApp tc tys) = all isTauTy tys && isTauTyCon tc
isTauTy (AppTy a b) = isTauTy a && isTauTy b
+isTauTy (FunTy InvisArg _ _) = False
isTauTy (FunTy _ a b) = isTauTy a && isTauTy b
isTauTy (ForAllTy {}) = False
isTauTy (CastTy ty _) = isTauTy ty
This change suffices to make d
be flagged as impredicative, and it passes GHC's test suite to boot. But then again, I'm unclear on the origins of the term "tau type"—perhaps it's permissible for tau types to have higher-rank contexts? If so, this suggests that we'd need to implement a variant of isTauTy
that checked for both contexts and forall
s.