Ignore unary constraint tuples during typechecking (#17511)

We deliberately avoid defining a magical `Unit%` class, for reasons
that I have expounded upon in the newly added
`Note [Ignore unary constraint tuples]` in `TcHsType`. However, a
sneaky user could try to insert `Unit%` into their program by way of
Template Haskell, leading to the interface-file error observed
in #17511. To avoid this, any time we encounter a unary constraint
tuple during typechecking, we drop the surrounding constraint tuple
application. This is safe to do since `Unit% a` and `a` would be
semantically equivalent (unlike other forms of unary tuples).

Fixes #17511.

3 files changed, 76 insertions, 25 deletions

diff --git a/compiler/basicTypes/BasicTypes.hs b/compiler/basicTypes/BasicTypes.hs
index ce449b3562..3763611349 100644
--- a/compiler/basicTypes/BasicTypes.hs
+++ b/compiler/basicTypes/BasicTypes.hs
@@ -821,6 +821,13 @@ data TupleSort
   | ConstraintTuple
   deriving( Eq, Data )
 
+instance Outputable TupleSort where
+  ppr ts = text $
+    case ts of
+      BoxedTuple      -> "BoxedTuple"
+      UnboxedTuple    -> "UnboxedTuple"
+      ConstraintTuple -> "ConstraintTuple"
+
 tupleSortBoxity :: TupleSort -> Boxity
 tupleSortBoxity BoxedTuple      = Boxed
 tupleSortBoxity UnboxedTuple    = Unboxed
diff --git a/compiler/prelude/TysWiredIn.hs b/compiler/prelude/TysWiredIn.hs
index de7ec7ec81..ba427efee7 100644
--- a/compiler/prelude/TysWiredIn.hs
+++ b/compiler/prelude/TysWiredIn.hs
@@ -722,9 +722,9 @@ created in Template Haskell or in, e.g., `deriving` code. There is
 nothing special about one-tuples in Core; in particular, they have no
 custom pretty-printing, just using `Unit`.
 
-NB (Feb 16): for /constraint/ one-tuples I have 'Unit%' but no class
-decl in GHC.Classes, so I think this part may not work properly. But
-it's unused I think.
+Note that there is *not* a unary constraint tuple, unlike for other forms of
+tuples. See [Ignore unary constraint tuples] in TcHsType for more
+details.
 
 See also Note [Flattening one-tuples] in MkCore and
 Note [Don't flatten tuples from HsSyn] in MkCore.
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 9a5d745dea..9f688f918a 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -947,30 +947,34 @@ finish_tuple :: HsType GhcRn
              -> [TcKind]    -- ^ of these kinds
              -> TcKind      -- ^ expected kind of the whole tuple
              -> TcM TcType
-finish_tuple rn_ty tup_sort tau_tys tau_kinds exp_kind
-  = do { traceTc "finish_tuple" (ppr res_kind $$ ppr tau_kinds $$ ppr exp_kind)
-       ; let arg_tys  = case tup_sort of
-                   -- See also Note [Unboxed tuple RuntimeRep vars] in TyCon
-                 UnboxedTuple    -> tau_reps ++ tau_tys
-                 BoxedTuple      -> tau_tys
-                 ConstraintTuple -> tau_tys
-       ; tycon <- case tup_sort of
-           ConstraintTuple
-             | arity > mAX_CTUPLE_SIZE
-                         -> failWith (bigConstraintTuple arity)
-             | otherwise -> tcLookupTyCon (cTupleTyConName arity)
-           BoxedTuple    -> do { let tc = tupleTyCon Boxed arity
-                               ; checkWiredInTyCon tc
-                               ; return tc }
-           UnboxedTuple  -> return (tupleTyCon Unboxed arity)
-       ; checkExpectedKind rn_ty (mkTyConApp tycon arg_tys) res_kind exp_kind }
+finish_tuple rn_ty tup_sort tau_tys tau_kinds exp_kind = do
+  traceTc "finish_tuple" (ppr tup_sort $$ ppr tau_kinds $$ ppr exp_kind)
+  case tup_sort of
+    ConstraintTuple
+      |  [tau_ty] <- tau_tys
+         -- Drop any uses of 1-tuple constraints here.
+         -- See Note [Ignore unary constraint tuples]
+      -> check_expected_kind tau_ty constraintKind
+      |  arity > mAX_CTUPLE_SIZE
+      -> failWith (bigConstraintTuple arity)
+      |  otherwise
+      -> do tycon <- tcLookupTyCon (cTupleTyConName arity)
+            check_expected_kind (mkTyConApp tycon tau_tys) constraintKind
+    BoxedTuple -> do
+      let tycon = tupleTyCon Boxed arity
+      checkWiredInTyCon tycon
+      check_expected_kind (mkTyConApp tycon tau_tys) liftedTypeKind
+    UnboxedTuple ->
+      let tycon    = tupleTyCon Unboxed arity
+          tau_reps = map kindRep tau_kinds
+          -- See also Note [Unboxed tuple RuntimeRep vars] in TyCon
+          arg_tys  = tau_reps ++ tau_tys
+          res_kind = unboxedTupleKind tau_reps in
+      check_expected_kind (mkTyConApp tycon arg_tys) res_kind
   where
     arity = length tau_tys
-    tau_reps = map kindRep tau_kinds
-    res_kind = case tup_sort of
-                 UnboxedTuple    -> unboxedTupleKind tau_reps
-                 BoxedTuple      -> liftedTypeKind
-                 ConstraintTuple -> constraintKind
+    check_expected_kind ty act_kind =
+      checkExpectedKind rn_ty ty act_kind exp_kind
 
 bigConstraintTuple :: Arity -> MsgDoc
 bigConstraintTuple arity
@@ -978,6 +982,46 @@ bigConstraintTuple arity
           <+> parens (text "max arity =" <+> int mAX_CTUPLE_SIZE))
        2 (text "Instead, use a nested tuple")
 
+{-
+Note [Ignore unary constraint tuples]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+GHC provides unary tuples and unboxed tuples (see Note [One-tuples] in
+TysWiredIn) but does *not* provide unary constraint tuples. Why? First,
+recall the definition of a unary tuple data type:
+
+  data Unit a = Unit a
+
+Note that `Unit a` is *not* the same thing as `a`, since Unit is boxed and
+lazy. Therefore, the presence of `Unit` matters semantically. On the other
+hand, suppose we had a unary constraint tuple:
+
+  class a => Unit% a
+
+This compiles down a newtype (i.e., a cast) in Core, so `Unit% a` is
+semantically equivalent to `a`. Therefore, a 1-tuple constraint would have
+no user-visible impact, nor would it allow you to express anything that
+you couldn't otherwise.
+
+We could simply add Unit% for consistency with tuples (Unit) and unboxed
+tuples (Unit#), but that would require even more magic to wire in another
+magical class, so we opt not to do so. We must be careful, however, since
+one can try to sneak in uses of unary constraint tuples through Template
+Haskell, such as in this program (from #17511):
+
+  f :: $(pure (ForallT [] [TupleT 1 `AppT` (ConT ''Show `AppT` ConT ''Int)]
+                       (ConT ''String)))
+  -- f :: Unit% (Show Int) => String
+  f = "abc"
+
+This use of `TupleT 1` will produce an HsBoxedOrConstraintTuple of arity 1,
+and since it is used in a Constraint position, GHC will attempt to treat
+it as thought it were a constraint tuple, which can potentially lead to
+trouble if one attempts to look up the name of a constraint tuple of arity
+1 (as it won't exist). To avoid this trouble, we simply take any unary
+constraint tuples discovered when typechecking and drop them—i.e., treat
+"Unit% a" as though the user had written "a". This is always safe to do
+since the two constraints should be semantically equivalent.
+-}
 
 {- *********************************************************************
 *                                                                      *