Commit cc495d57 authored by Ryan Scott's avatar Ryan Scott Committed by Ömer Sinan Ağacan

Make equality constraints in kinds invisible

Issues #12102 and #15872 revealed something strange about the way GHC
handles equality constraints in kinds: it treats them as _visible_
arguments! This causes a litany of strange effects, from strange
error messages
(ghc/ghc#12102 (comment 169035))
to bizarre `Eq#`-related things leaking through to GHCi output, even
without any special flags enabled.

This patch is an attempt to contain some of this strangeness.
In particular:

* In `TcHsType.etaExpandAlgTyCon`, we propagate through the
  `AnonArgFlag`s of any `Anon` binders. Previously, we were always
  hard-coding them to `VisArg`, which meant that invisible binders
  (like those whose kinds were equality constraint) would mistakenly
  get flagged as visible.
* In `ToIface.toIfaceAppArgsX`, we previously assumed that the
  argument to a `FunTy` always corresponding to a `Required`
  argument. We now dispatch on the `FunTy`'s `AnonArgFlag` and map
  `VisArg` to `Required` and `InvisArg` to `Inferred`. As a
  consequence, the iface pretty-printer correctly recognizes that
  equality coercions are inferred arguments, and as a result,
  only displays them in `-fprint-explicit-kinds` is enabled.
* Speaking of iface pretty-printing, `Anon InvisArg` binders were
  previously being pretty-printed like `T (a :: b ~ c)`, as if they
  were required. This seemed inconsistent with other invisible
  arguments (that are printed like `T @{d}`), so I decided to switch
  this to `T @{a :: b ~ c}`.

Along the way, I also cleaned up a minor inaccuracy in the users'
guide section for constraints in kinds that was spotted in
ghc/ghc#12102 (comment 136220).

Fixes #12102 and #15872.
parent 87bc954a
......@@ -719,8 +719,9 @@ pprIfaceTyConBinders = sep . map go
-- See Note [Pretty-printing invisible arguments]
case vis of
AnonTCB VisArg -> ppr_bndr True
AnonTCB InvisArg -> ppr_bndr True -- Rare; just promoted GADT data constructors
-- Should we print them differently?
AnonTCB InvisArg -> char '@' <> braces (ppr_bndr False)
-- The above case is rare. (See Note [AnonTCB InvisArg] in TyCon.)
-- Should we print these differently?
NamedTCB Required -> ppr_bndr True
NamedTCB Specified -> char '@' <> ppr_bndr True
NamedTCB Inferred -> char '@' <> braces (ppr_bndr False)
......
......@@ -309,8 +309,14 @@ toIfaceAppArgsX fr kind ty_args
t' = toIfaceTypeX fr t
ts' = go (extendTCvSubst env tv t) res ts
go env (FunTy { ft_res = res }) (t:ts) -- No type-class args in tycon apps
= IA_Arg (toIfaceTypeX fr t) Required (go env res ts)
go env (FunTy { ft_af = af, ft_res = res }) (t:ts)
= IA_Arg (toIfaceTypeX fr t) argf (go env res ts)
where
argf = case af of
VisArg -> Required
InvisArg -> Inferred
-- It's rare for a kind to have a constraint argument, but
-- it can happen. See Note [AnonTCB InvisArg] in TyCon.
go env ty ts@(t1:ts1)
| not (isEmptyTCvSubst env)
......
......@@ -2368,13 +2368,13 @@ etaExpandAlgTyCon tc_bndrs kind
= case splitPiTy_maybe kind of
Nothing -> (reverse acc, substTy subst kind)
Just (Anon _ arg, kind')
Just (Anon af arg, kind')
-> go loc occs' uniqs' subst' (tcb : acc) kind'
where
arg' = substTy subst arg
tv = mkTyVar (mkInternalName uniq occ loc) arg'
subst' = extendTCvInScope subst tv
tcb = Bndr tv (AnonTCB VisArg)
tcb = Bndr tv (AnonTCB af)
(uniq:uniqs') = uniqs
(occ:occs') = occs
......
......@@ -487,14 +487,22 @@ tyConVisibleTyVars tc
= [ tv | Bndr tv vis <- tyConBinders tc
, isVisibleTcbVis vis ]
{- Note [AnonTCB InivsArg]
{- Note [AnonTCB InvisArg]
~~~~~~~~~~~~~~~~~~~~~~~~~~
It's pretty rare to have an (AnonTCB InvisArg) binder. The
only way it can occur is in a PromotedDataCon whose
kind has an equality constraint:
'MkT :: forall a b. (a~b) => blah
See Note [Constraints in kinds] in TyCoRep, and
Note [Promoted data constructors] in this module.
only way it can occur is through equality constraints in kinds. These
can arise in one of two ways:
* In a PromotedDataCon whose kind has an equality constraint:
'MkT :: forall a b. (a~b) => blah
See Note [Constraints in kinds] in TyCoRep, and
Note [Promoted data constructors] in this module.
* In a data type whose kind has an equality constraint, as in the
following example from #12102:
data T :: forall a. (IsTypeLit a ~ 'True) => a -> Type
When mapping an (AnonTCB InvisArg) to an ArgFlag, in
tyConBndrVisArgFlag, we use "Inferred" to mean "the user cannot
......
......@@ -9395,7 +9395,8 @@ Here is an example of a constrained kind: ::
The declarations above are accepted. However, if we add ``MkOther :: T Int``,
we get an error that the equality constraint is not satisfied; ``Int`` is
not a type literal. Note that explicitly quantifying with ``forall a`` is
not necessary here.
necessary in order for ``T`` to typecheck
(see :ref:`complete-kind-signatures`).
The kind ``Type``
-----------------
......@@ -10351,13 +10352,13 @@ function that can *never* be called, such as this one: ::
f :: (Int ~ Bool) => a -> a
Sometimes :extension:`AllowAmbiguousTypes` does not mix well with :extension:`RankNTypes`.
For example: ::
For example: ::
foo :: forall r. (forall i. (KnownNat i) => r) -> r
foo f = f @1
boo :: forall j. (KnownNat j) => Int
boo = ....
h :: Int
h = foo boo
......@@ -10367,7 +10368,7 @@ the type variables `j` and `i`.
Unlike the previous examples, it is not currently possible
to resolve the ambiguity manually by using :extension:`TypeApplications`.
.. note::
*A historical note.* GHC used to impose some more restrictive and less
principled conditions on type signatures. For type
......
{-# Language RankNTypes #-}
{-# Language DataKinds #-}
{-# Language PolyKinds #-}
{-# Language GADTs #-}
module T15872 where
import Data.Kind
data WHICH = OP | OPOP
data Fun :: forall (a :: WHICH). a ~ OP => Type -> Type -> Type where
MkFun :: (a -> b) -> Fun a b
:l T15872
:t MkFun
:k Fun
:i Fun
:set -fprint-explicit-kinds
:t MkFun
:k Fun
:i Fun
MkFun :: (a -> b) -> Fun a b
Fun :: (a ~ 'OP) => * -> * -> *
data Fun b c where
MkFun :: (b -> c) -> Fun b c
-- Defined at T15872.hs:11:1
MkFun
:: (a -> b) -> Fun @'OP @{'GHC.Types.Eq# @WHICH @'OP @'OP <>} a b
Fun :: ((a :: WHICH) ~ ('OP :: WHICH)) => * -> * -> *
type role Fun nominal nominal representational representational
data Fun @(a :: WHICH)
@{a1 :: (a :: WHICH) ~ ('OP :: WHICH)}
b
c where
MkFun :: (b -> c)
-> Fun @'OP @{'GHC.Types.Eq# @WHICH @'OP @'OP <>} b c
-- Defined at T15872.hs:11:1
......@@ -287,6 +287,7 @@ test('T15325', normal, ghci_script, ['T15325.script'])
test('T15591', normal, ghci_script, ['T15591.script'])
test('T15743b', normal, ghci_script, ['T15743b.script'])
test('T15827', normal, ghci_script, ['T15827.script'])
test('T15872', normal, ghci_script, ['T15872.script'])
test('T15898', normal, ghci_script, ['T15898.script'])
test('T15941', normal, ghci_script, ['T15941.script'])
test('T16030', normal, ghci_script, ['T16030.script'])
......
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
module T12102b where
import Data.Kind
import GHC.TypeLits
type family IsTypeLit a where
IsTypeLit Nat = 'True
IsTypeLit Symbol = 'True
IsTypeLit a = 'False
data T :: forall a. (IsTypeLit a ~ 'True) => a -> Type where
MkNat :: T 42
MkSymbol :: T "Don't panic!"
deriving instance Show (T a)
T12102b.hs:21:25: error:
• Couldn't match expected kind ‘'True’
with actual kind ‘IsTypeLit a0’
The type variable ‘a0’ is ambiguous
• In the first argument of ‘Show’, namely ‘(T a)’
In the stand-alone deriving instance for ‘Show (T a)’
......@@ -411,6 +411,7 @@ test('T12083a', normal, compile_fail, [''])
test('T12083b', normal, compile_fail, [''])
test('T11974b', normal, compile_fail, [''])
test('T12102', normal, compile, [''])
test('T12102b', normal, compile_fail, [''])
test('T12151', normal, compile_fail, [''])
test('T7437', normal, compile_fail, [''])
test('T12177', normal, compile_fail, [''])
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment