From 62ce23f785fc735fa80f563d66db65e48bb0610d Mon Sep 17 00:00:00 2001
From: Jan Stolarek <jan.stolarek@p.lodz.pl>
Date: Sat, 9 Jan 2016 20:58:52 +0100
Subject: [PATCH] Add InjectiveTypeFamilies language extension
Previously injective type families were part of TypeFamilies.
Now they are in a separate language extension.
Test Plan: ./validate
Reviewers: austin, bgamari, goldfire
Reviewed By: bgamari
Subscribers: goldfire, thomie
Differential Revision: https://phabricator.haskell.org/D1750
GHC Trac Issues: #11381
(cherry picked from commit fbd6de2f0761b63a5f0a88ce0590f515d63790a4)
---
compiler/main/DynFlags.hs | 4 +++-
compiler/typecheck/TcTyClsDecls.hs | 6 +++++-
compiler/typecheck/TcValidity.hs | 2 +-
docs/users_guide/glasgow_exts.rst | 3 +++
libraries/ghc-boot/GHC/LanguageExtensions.hs | 1 +
testsuite/tests/driver/T11381.hs | 9 +++++++++
testsuite/tests/driver/T11381.stderr | 5 +++++
testsuite/tests/driver/T4437.hs | 3 ++-
testsuite/tests/driver/all.T | 1 +
testsuite/tests/ghci/scripts/T6018ghci.script | 2 +-
testsuite/tests/ghci/scripts/T6018ghcifail.script | 2 +-
testsuite/tests/ghci/scripts/T6018ghcirnfail.script | 2 +-
testsuite/tests/th/T6018th.hs | 4 ++--
testsuite/tests/th/T8884.hs | 2 +-
testsuite/tests/typecheck/should_compile/T6018.hs | 2 +-
testsuite/tests/typecheck/should_compile/T6018.hs-boot | 2 +-
testsuite/tests/typecheck/should_compile/T6018a.hs | 2 +-
testsuite/tests/typecheck/should_fail/T10836.hs | 2 +-
testsuite/tests/typecheck/should_fail/T6018Afail.hs | 2 +-
testsuite/tests/typecheck/should_fail/T6018Bfail.hs | 2 +-
testsuite/tests/typecheck/should_fail/T6018fail.hs | 2 +-
testsuite/tests/typecheck/should_fail/T6018failclosed.hs | 4 ++--
.../tests/typecheck/should_fail/T6018failclosed2.hs | 2 +-
utils/mkUserGuidePart/Options/Language.hs | 8 ++++++++
24 files changed, 54 insertions(+), 20 deletions(-)
create mode 100644 testsuite/tests/driver/T11381.hs
create mode 100644 testsuite/tests/driver/T11381.stderr
diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index 3caff6355351..fea441cf21c6 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -243,7 +243,7 @@ import qualified GHC.LanguageExtensions as LangExt
--
-- * Adding the extension to GHC.LanguageExtensions
--
--- The LangExt type in libraries/ghc-boot/GHC/LanguageExtensions.hs is
+-- The Extension type in libraries/ghc-boot/GHC/LanguageExtensions.hs is
-- the canonical list of language extensions known by GHC.
--
-- * Adding a flag to DynFlags.xFlags
@@ -3213,6 +3213,7 @@ xFlags = [
flagSpec "ImpredicativeTypes" LangExt.ImpredicativeTypes,
flagSpec' "IncoherentInstances" LangExt.IncoherentInstances
setIncoherentInsts,
+ flagSpec "InjectiveTypeFamilies" LangExt.InjectiveTypeFamilies,
flagSpec "InstanceSigs" LangExt.InstanceSigs,
flagSpec "ApplicativeDo" LangExt.ApplicativeDo,
flagSpec "InterruptibleFFI" LangExt.InterruptibleFFI,
@@ -3352,6 +3353,7 @@ impliedXFlags
, (LangExt.FlexibleInstances, turnOn, LangExt.TypeSynonymInstances)
, (LangExt.FunctionalDependencies, turnOn, LangExt.MultiParamTypeClasses)
, (LangExt.MultiParamTypeClasses, turnOn, LangExt.ConstrainedClassMethods) -- c.f. Trac #7854
+ , (LangExt.InjectiveTypeFamilies, turnOn, LangExt.TypeFamilies)
, (LangExt.RebindableSyntax, turnOff, LangExt.ImplicitPrelude) -- NB: turn off!
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 4424304a431c..40501a3443a3 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -834,7 +834,11 @@ tcInjectivity _ Nothing
-- reason is that the implementation would not be straightforward.)
tcInjectivity tvs (Just (L loc (InjectivityAnn _ lInjNames)))
= setSrcSpan loc $
- do { inj_tvs <- mapM (tcLookupTyVar . unLoc) lInjNames
+ do { dflags <- getDynFlags
+ ; checkTc (xopt LangExt.InjectiveTypeFamilies dflags)
+ (text "Illegal injectivity annotation" $$
+ text "Use InjectiveTypeFamilies to allow this")
+ ; inj_tvs <- mapM (tcLookupTyVar . unLoc) lInjNames
; let inj_ktvs = filterVarSet isTyVar $ -- no injective coercion vars
closeOverKinds (mkVarSet inj_tvs)
; let inj_bools = map (`elemVarSet` inj_ktvs) tvs
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 98b78db4501f..2df092bd4455 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -1328,7 +1328,7 @@ checkValidCoAxiom ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches })
-> CoAxBranch -- current branch
-> TcM [CoAxBranch]-- current branch : previous branches
-- Check for
- -- (a) this banch is dominated by previous ones
+ -- (a) this branch is dominated by previous ones
-- (b) failure of injectivity
check_branch_compat prev_branches cur_branch
| cur_branch `isDominatedBy` prev_branches
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 93686602442f..7d37c6386ad6 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -6764,6 +6764,9 @@ will be possible to infer ``t`` at call sites from the type of the argument: ::
type family Id a = r | r -> a
+Injective type families are enabled with ``-XInjectiveTypeFamilies`` language
+extension. This extension implies ``-XTypeFamilies``.
+
For full details on injective type families refer to Haskell Symposium
2015 paper `Injective type families for
Haskell <http://ics.p.lodz.pl/~stolarek/_media/pl:research:stolarek_peyton-jones_eisenberg_injectivity_extended.pdf>`__.
diff --git a/libraries/ghc-boot/GHC/LanguageExtensions.hs b/libraries/ghc-boot/GHC/LanguageExtensions.hs
index 68455194e651..0ccd59cbb07c 100644
--- a/libraries/ghc-boot/GHC/LanguageExtensions.hs
+++ b/libraries/ghc-boot/GHC/LanguageExtensions.hs
@@ -45,6 +45,7 @@ data Extension
| UnboxedTuples
| BangPatterns
| TypeFamilies
+ | InjectiveTypeFamilies
| TypeInType
| OverloadedStrings
| OverloadedLists
diff --git a/testsuite/tests/driver/T11381.hs b/testsuite/tests/driver/T11381.hs
new file mode 100644
index 000000000000..8dc94dd8a798
--- /dev/null
+++ b/testsuite/tests/driver/T11381.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T11381 where
+
+-- ensure that this code does not compile without InjectiveTypeFamilies and that
+-- injectivity error is not reported.
+type family F a = r | r -> a
+type instance F Int = Bool
+type instance F Int = Char
diff --git a/testsuite/tests/driver/T11381.stderr b/testsuite/tests/driver/T11381.stderr
new file mode 100644
index 000000000000..afe652d38e4b
--- /dev/null
+++ b/testsuite/tests/driver/T11381.stderr
@@ -0,0 +1,5 @@
+
+T11381.hs:7:23:
+ Illegal injectivity annotation
+ Use InjectiveTypeFamilies to allow this
+ In the type family declaration for ‘F’
diff --git a/testsuite/tests/driver/T4437.hs b/testsuite/tests/driver/T4437.hs
index 5f14da1a9a0d..cbf71868bdc3 100644
--- a/testsuite/tests/driver/T4437.hs
+++ b/testsuite/tests/driver/T4437.hs
@@ -38,7 +38,8 @@ check title expected got
expectedGhcOnlyExtensions :: [String]
expectedGhcOnlyExtensions = ["RelaxedLayout",
"AlternativeLayoutRule",
- "AlternativeLayoutRuleTransitional"]
+ "AlternativeLayoutRuleTransitional",
+ "InjectiveTypeFamilies"]
expectedCabalOnlyExtensions :: [String]
expectedCabalOnlyExtensions = ["Generics",
diff --git a/testsuite/tests/driver/all.T b/testsuite/tests/driver/all.T
index 8493aa4c5770..e0022d7d6092 100644
--- a/testsuite/tests/driver/all.T
+++ b/testsuite/tests/driver/all.T
@@ -466,3 +466,4 @@ test('T10970', normal, compile_and_run, ['-hide-all-packages -package base -pack
test('T10970a', normal, compile_and_run, [''])
test('T4931', normal, compile_and_run, [''])
test('T11182', normal, compile_and_run, [''])
+test('T11381', normal, compile_fail, [''])
diff --git a/testsuite/tests/ghci/scripts/T6018ghci.script b/testsuite/tests/ghci/scripts/T6018ghci.script
index 4615be2d041e..3b14bd346747 100644
--- a/testsuite/tests/ghci/scripts/T6018ghci.script
+++ b/testsuite/tests/ghci/scripts/T6018ghci.script
@@ -1,4 +1,4 @@
-:set -XTypeFamilies
+:set -XInjectiveTypeFamilies
:set -XDataKinds
:set -XUndecidableInstances
:set -XPolyKinds
diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.script b/testsuite/tests/ghci/scripts/T6018ghcifail.script
index c0e073457f7a..0e6fe6503335 100644
--- a/testsuite/tests/ghci/scripts/T6018ghcifail.script
+++ b/testsuite/tests/ghci/scripts/T6018ghcifail.script
@@ -1,4 +1,4 @@
-:set -XTypeFamilies
+:set -XInjectiveTypeFamilies
:set -XDataKinds
:set -XUndecidableInstances
:set -XPolyKinds
diff --git a/testsuite/tests/ghci/scripts/T6018ghcirnfail.script b/testsuite/tests/ghci/scripts/T6018ghcirnfail.script
index f1a5fa469a3c..1f3372ebaca6 100644
--- a/testsuite/tests/ghci/scripts/T6018ghcirnfail.script
+++ b/testsuite/tests/ghci/scripts/T6018ghcirnfail.script
@@ -1,4 +1,4 @@
-:set -XTypeFamilies
+:set -XInjectiveTypeFamilies
:set -XDataKinds
:set -XUndecidableInstances
:set -XPolyKinds
diff --git a/testsuite/tests/th/T6018th.hs b/testsuite/tests/th/T6018th.hs
index 62af74383563..1643e9aea5f3 100644
--- a/testsuite/tests/th/T6018th.hs
+++ b/testsuite/tests/th/T6018th.hs
@@ -1,5 +1,5 @@
-{-# LANGUAGE TypeFamilies, DataKinds, UndecidableInstances, PolyKinds #-}
-
+{-# LANGUAGE InjectiveTypeFamilies, DataKinds, UndecidableInstances,
+ PolyKinds #-}
module T6018th where
import Language.Haskell.TH
diff --git a/testsuite/tests/th/T8884.hs b/testsuite/tests/th/T8884.hs
index 4255f76a4d2f..cad38f9de18b 100644
--- a/testsuite/tests/th/T8884.hs
+++ b/testsuite/tests/th/T8884.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TemplateHaskell, TypeFamilies, PolyKinds #-}
+{-# LANGUAGE TemplateHaskell, InjectiveTypeFamilies, PolyKinds #-}
module T8884 where
diff --git a/testsuite/tests/typecheck/should_compile/T6018.hs b/testsuite/tests/typecheck/should_compile/T6018.hs
index 523bc968d00a..62894c791a03 100644
--- a/testsuite/tests/typecheck/should_compile/T6018.hs
+++ b/testsuite/tests/typecheck/should_compile/T6018.hs
@@ -1,7 +1,7 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE InjectiveTypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
diff --git a/testsuite/tests/typecheck/should_compile/T6018.hs-boot b/testsuite/tests/typecheck/should_compile/T6018.hs-boot
index e31903a3121e..d1cb0687cc2f 100644
--- a/testsuite/tests/typecheck/should_compile/T6018.hs-boot
+++ b/testsuite/tests/typecheck/should_compile/T6018.hs-boot
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, PolyKinds #-}
+{-# LANGUAGE InjectiveTypeFamilies, PolyKinds #-}
module T6018 where
diff --git a/testsuite/tests/typecheck/should_compile/T6018a.hs b/testsuite/tests/typecheck/should_compile/T6018a.hs
index beecb57c6588..e1e40bb790f8 100644
--- a/testsuite/tests/typecheck/should_compile/T6018a.hs
+++ b/testsuite/tests/typecheck/should_compile/T6018a.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE InjectiveTypeFamilies #-}
module T6018a where
diff --git a/testsuite/tests/typecheck/should_fail/T10836.hs b/testsuite/tests/typecheck/should_fail/T10836.hs
index 00c5c6a650f0..3ad2093c924a 100644
--- a/testsuite/tests/typecheck/should_fail/T10836.hs
+++ b/testsuite/tests/typecheck/should_fail/T10836.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE InjectiveTypeFamilies #-}
module T10836 where
type family Foo a = r | r -> a where
diff --git a/testsuite/tests/typecheck/should_fail/T6018Afail.hs b/testsuite/tests/typecheck/should_fail/T6018Afail.hs
index 95184a177c08..d0cc076ac691 100644
--- a/testsuite/tests/typecheck/should_fail/T6018Afail.hs
+++ b/testsuite/tests/typecheck/should_fail/T6018Afail.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE InjectiveTypeFamilies #-}
module T6018Afail where
diff --git a/testsuite/tests/typecheck/should_fail/T6018Bfail.hs b/testsuite/tests/typecheck/should_fail/T6018Bfail.hs
index ef2460187ff3..2b7b4427693d 100644
--- a/testsuite/tests/typecheck/should_fail/T6018Bfail.hs
+++ b/testsuite/tests/typecheck/should_fail/T6018Bfail.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE InjectiveTypeFamilies #-}
module T6018Bfail where
diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.hs b/testsuite/tests/typecheck/should_fail/T6018fail.hs
index ead4dd354fc3..8531c13d9ad7 100644
--- a/testsuite/tests/typecheck/should_fail/T6018fail.hs
+++ b/testsuite/tests/typecheck/should_fail/T6018fail.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, DataKinds, UndecidableInstances, PolyKinds,
+{-# LANGUAGE InjectiveTypeFamilies, DataKinds, UndecidableInstances, PolyKinds,
MultiParamTypeClasses, FlexibleInstances #-}
module T6018fail where
diff --git a/testsuite/tests/typecheck/should_fail/T6018failclosed.hs b/testsuite/tests/typecheck/should_fail/T6018failclosed.hs
index a69c63f7e5c1..eed5d033fb5d 100644
--- a/testsuite/tests/typecheck/should_fail/T6018failclosed.hs
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed.hs
@@ -1,5 +1,5 @@
-{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, UndecidableInstances #-}
-
+{-# LANGUAGE InjectiveTypeFamilies, DataKinds, PolyKinds,
+ UndecidableInstances #-}
module T6018failclosed where
-- Id is injective...
diff --git a/testsuite/tests/typecheck/should_fail/T6018failclosed2.hs b/testsuite/tests/typecheck/should_fail/T6018failclosed2.hs
index d90b9decfc0f..323b16fde34c 100644
--- a/testsuite/tests/typecheck/should_fail/T6018failclosed2.hs
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed2.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE InjectiveTypeFamilies #-}
module T6018failclosed2 where
diff --git a/utils/mkUserGuidePart/Options/Language.hs b/utils/mkUserGuidePart/Options/Language.hs
index 0fc3ea5f2520..ddd05ea13f1f 100644
--- a/utils/mkUserGuidePart/Options/Language.hs
+++ b/utils/mkUserGuidePart/Options/Language.hs
@@ -340,6 +340,14 @@ languageOptions =
, flagReverse = "-XNoIncoherentInstances"
, flagSince = "6.8.1"
}
+ , flag { flagName = "-XInjectiveTypeFamilies"
+ , flagDescription =
+ "Enable :ref:`injective type families <injective-ty-fams>`. "++
+ "Implies ``-XTypeFamilies``."
+ , flagType = DynamicFlag
+ , flagReverse = "-XNoInjectiveTypeFamilies"
+ , flagSince = "8.0.1"
+ }
, flag { flagName = "-XInstanceSigs"
, flagDescription =
"Enable :ref:`instance signatures <instance-sigs>`."
--
GitLab