[commit: ghc] master: Suggest how to fix illegally nested foralls in GADT constructor type signatures (039fa1b)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/039fa1b994a8b0d6be25eb1bc711904db9661db2/ghc

>---------------------------------------------------------------

commit 039fa1b994a8b0d6be25eb1bc711904db9661db2
Author: Ryan Scott <ryan.gl.scott at gmail.com>
Date:   Thu Aug 17 10:07:03 2017 -0400

    Suggest how to fix illegally nested foralls in GADT constructor type signatures
    
    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


>---------------------------------------------------------------

039fa1b994a8b0d6be25eb1bc711904db9661db2
 compiler/typecheck/TcTyClsDecls.hs | 43 ++++++++++++++++++++++++++++++++++++++
 testsuite/tests/gadt/T12087.hs     | 18 ++++++++++++++++
 testsuite/tests/gadt/T12087.stderr | 35 +++++++++++++++++++++++++++++++
 testsuite/tests/gadt/all.T         |  1 +
 4 files changed, 97 insertions(+)

diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index ba35db5..0974fe5 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -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
index 0000000..e56240c
--- /dev/null
+++ b/testsuite/tests/gadt/T12087.hs
@@ -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
index 0000000..03f2465
--- /dev/null
+++ b/testsuite/tests/gadt/T12087.stderr
@@ -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’
diff --git a/testsuite/tests/gadt/all.T b/testsuite/tests/gadt/all.T
index 877943b..3c825f0 100644
--- a/testsuite/tests/gadt/all.T
+++ b/testsuite/tests/gadt/all.T
@@ -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, [''])