Suggest how to fix illegally nested foralls in GADT constructor type signatures
authorRyan Scott <ryan.gl.scott@gmail.com>
Thu, 17 Aug 2017 14:07:03 +0000 (10:07 -0400)
committerRyan Scott <ryan.gl.scott@gmail.com>
Thu, 17 Aug 2017 14:07:03 +0000 (10:07 -0400)
Summary:
Although the code from #12087 isn't accepted by GHC, we can at least
do a better job of letting users know what the problem is, and how to fix it.

Test Plan: make test TEST=T12087

Reviewers: goldfire, austin, bgamari

Reviewed By: goldfire

Subscribers: rwbarton, thomie

GHC Trac Issues: #12087

Differential Revision: https://phabricator.haskell.org/D3851

compiler/typecheck/TcTyClsDecls.hs
testsuite/tests/gadt/T12087.hs [new file with mode: 0644]
testsuite/tests/gadt/T12087.stderr [new file with mode: 0644]
testsuite/tests/gadt/all.T

index ba35db5..0974fe5 100644 (file)
@@ -3138,9 +3138,52 @@ noClassTyVarErr clas fam_tc
 
 badDataConTyCon :: DataCon -> Type -> Type -> SDoc
 badDataConTyCon data_con res_ty_tmpl actual_res_ty
+  | tcIsForAllTy actual_res_ty
+  = nested_foralls_contexts_suggestion
+  | isJust (tcSplitPredFunTy_maybe actual_res_ty)
+  = nested_foralls_contexts_suggestion
+  | otherwise
   = hang (text "Data constructor" <+> quotes (ppr data_con) <+>
                 text "returns type" <+> quotes (ppr actual_res_ty))
        2 (text "instead of an instance of its parent type" <+> quotes (ppr res_ty_tmpl))
+  where
+    -- This suggestion is useful for suggesting how to correct code like what
+    -- was reported in Trac #12087:
+    --
+    --   data F a where
+    --     MkF :: Ord a => Eq a => a -> F a
+    --
+    -- Although nested foralls or contexts are allowed in function type
+    -- signatures, it is much more difficult to engineer GADT constructor type
+    -- signatures to allow something similar, so we error in the latter case.
+    -- Nevertheless, we can at least suggest how a user might reshuffle their
+    -- exotic GADT constructor type signature so that GHC will accept.
+    nested_foralls_contexts_suggestion =
+      text "GADT constructor type signature cannot contain nested"
+      <+> quotes forAllLit <> text "s or contexts"
+      $+$ hang (text "Suggestion: instead use this type signature:")
+             2 (ppr (dataConName data_con) <+> dcolon <+> ppr suggested_ty)
+
+    -- To construct a type that GHC would accept (suggested_ty), we:
+    --
+    -- 1) Find the existentially quantified type variables and the class
+    --    predicates from the datacon. (NB: We don't need the universally
+    --    quantified type variables, since rejigConRes won't substitute them in
+    --    the result type if it fails, as in this scenario.)
+    -- 2) Split apart the return type (which is headed by a forall or a
+    --    context) using tcSplitNestedSigmaTys, collecting the type variables
+    --    and class predicates we find, as well as the rho type lurking
+    --    underneath the nested foralls and contexts.
+    -- 3) Smash together the type variables and class predicates from 1) and
+    --    2), and prepend them to the rho type from 2).
+    actual_ex_tvs = dataConExTyVarBinders data_con
+    actual_theta  = dataConTheta data_con
+    (actual_res_tvs, actual_res_theta, actual_res_rho)
+      = tcSplitNestedSigmaTys actual_res_ty
+    actual_res_tvbs = mkTyVarBinders Specified actual_res_tvs
+    suggested_ty = mkForAllTys (actual_ex_tvs ++ actual_res_tvbs) $
+                   mkFunTys (actual_theta ++ actual_res_theta)
+                   actual_res_rho
 
 badGadtDecl :: Name -> SDoc
 badGadtDecl tc_name
diff --git a/testsuite/tests/gadt/T12087.hs b/testsuite/tests/gadt/T12087.hs
new file mode 100644 (file)
index 0000000..e56240c
--- /dev/null
@@ -0,0 +1,18 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+module T12087 where
+
+data F1 a where
+  MkF1 :: Ord a => Eq a => a -> F1 a
+
+data F2 a where
+  MkF2 :: Ord a => a -> Eq a => F2 a
+
+data F3 a where
+  MkF3 :: forall a. Eq a => a -> forall b. Eq b => b -> F3 a
+
+data F4 a where
+  MkF4 :: forall a b. Eq a => a -> Eq b => b -> F4 a
+
+data F5 a where
+  MkF5 :: Int -> Int -> forall a. a -> Int -> Int -> forall b. b -> F5 a
diff --git a/testsuite/tests/gadt/T12087.stderr b/testsuite/tests/gadt/T12087.stderr
new file mode 100644 (file)
index 0000000..03f2465
--- /dev/null
@@ -0,0 +1,35 @@
+
+T12087.hs:6:3: error:
+    • GADT constructor type signature cannot contain nested ‘forall’s or contexts
+      Suggestion: instead use this type signature:
+        MkF1 :: forall a. (Ord a, Eq a) => a -> F1 a
+    • In the definition of data constructor ‘MkF1’
+      In the data type declaration for ‘F1’
+
+T12087.hs:9:3: error:
+    • GADT constructor type signature cannot contain nested ‘forall’s or contexts
+      Suggestion: instead use this type signature:
+        MkF2 :: forall a. (Ord a, Eq a) => F2 a
+    • In the definition of data constructor ‘MkF2’
+      In the data type declaration for ‘F2’
+
+T12087.hs:12:3: error:
+    • GADT constructor type signature cannot contain nested ‘forall’s or contexts
+      Suggestion: instead use this type signature:
+        MkF3 :: forall a b. (Eq a, Eq b) => b -> F3 a
+    • In the definition of data constructor ‘MkF3’
+      In the data type declaration for ‘F3’
+
+T12087.hs:15:3: error:
+    • GADT constructor type signature cannot contain nested ‘forall’s or contexts
+      Suggestion: instead use this type signature:
+        MkF4 :: forall a b. (Eq a, Eq b) => b -> F4 a
+    • In the definition of data constructor ‘MkF4’
+      In the data type declaration for ‘F4’
+
+T12087.hs:18:3: error:
+    • GADT constructor type signature cannot contain nested ‘forall’s or contexts
+      Suggestion: instead use this type signature:
+        MkF5 :: forall a b. a -> Int -> Int -> b -> F5 a
+    • In the definition of data constructor ‘MkF5’
+      In the data type declaration for ‘F5’
index 877943b..3c825f0 100644 (file)
@@ -56,7 +56,7 @@ test('records-fail1', normal, compile_fail, [''])
 test('doaitse', normal, compile, [''])
 test('josef', normal, compile, [''])
 
-# Interaction of fundeps with GADTs doesn't work well 
+# Interaction of fundeps with GADTs doesn't work well
 test('gadt-fd', expect_broken(345), compile, [''])
 
 test('karl1', normal, compile, [''])
@@ -112,4 +112,5 @@ test('T7974', normal, compile, [''])
 test('T7558', normal, compile_fail, [''])
 test('T9096', normal, compile, [''])
 test('T9380', normal, compile_and_run, [''])
+test('T12087', normal, compile_fail, [''])
 test('T12468', normal, compile_fail, [''])