diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs index 3caff635535192beac398530df7c6d3f9e384008..fea441cf21c6a8019687d9da3db7da47f001c5c8 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 4424304a431c6911a0516fff26ba89ae35c06af6..40501a3443a3d4e28999f21b2f7a767b7c75b8ec 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 98b78db4501f6b3b07c39c96023fc29d380a10ee..2df092bd4455a00641d1d7da1c768dca1d4a1017 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 93686602442f50473bd5d398afb6b8505ced82fb..7d37c6386ad62483fda50795088d55bd7f63b226 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 68455194e651b0f0a51d8c1c6c9c4b60b2639a57..0ccd59cbb07c5edce8311f0ed5c1beba5d351301 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 0000000000000000000000000000000000000000..8dc94dd8a798d2a64a3422bf65a2d9b8b8c31ad9 --- /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 0000000000000000000000000000000000000000..afe652d38e4b9a8c2ab6acb062e1b4fb052628e7 --- /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 5f14da1a9a0d04a057f8bfa31c293c13326fbb13..cbf71868bdc3d6a2d1a7058e0819c57ac029e792 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 8493aa4c5770c2a1e6934c3d590cc6aa0997b67d..e0022d7d60922e6e6f97b14eeaf2b2ff39213075 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 4615be2d041eafd44619686710de87e8688f05f3..3b14bd3467473af61f581ed15a7aeb2b1371b26d 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 c0e073457f7a5229113671f26a0e8c6506dc1e7c..0e6fe6503335fc75e77e55f596e7e349cbb8ad57 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 f1a5fa469a3c663cd86d4ead3f069117420b007e..1f3372ebaca6725ee324249ffd1b614a4b0a31b8 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 62af743835637256dde4a22334ef40d15de46731..1643e9aea5f3d11e599b8f33ca236769aa64b922 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 4255f76a4d2f75366f430f3a4dcc9dec1324602c..cad38f9de18b748aeb97707f9249f607bbb08ecb 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 523bc968d00a18eedd1e03dfbd65abf74f11ea4f..62894c791a03e2a3d557e1807a6f2b76d65ce8e5 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 e31903a3121e2dbc83c4d604f8f5eee656acbbe2..d1cb0687cc2f0742c506e71033ed76ab7b9a0750 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 beecb57c65889ea7ebff4c6e96876cf59c90c056..e1e40bb790f800b4f4b959ccba1a6a9426653fe7 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 00c5c6a650f09da398f2eb71a82f1a298dbefcca..3ad2093c924a0eb5dbec7ee9dbcd2da6ccfb95c4 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 95184a177c088847deca2cce347bc24abb8a6169..d0cc076ac691845e98bcc18f11ab178160a59cc3 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 ef2460187ff305a50ba31661fe8d46744ece60dc..2b7b4427693d1abeb900a18f49875624b45226a7 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 ead4dd354fc389ffeaa9aac6d81f2ddde45bcd39..8531c13d9ad7e2a06ab78f90e101eaa3059f1a43 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 a69c63f7e5c173ffd66ab04ff28b68978f1328b6..eed5d033fb5d0c3100922d73386a769bd581dd57 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 d90b9decfc0fbac78863fd0e61f2ef72d6f0020c..323b16fde34c30f0514842e13840d6bf5ae5e6e8 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 0fc3ea5f25209c50c874b9cb950a09a79aecb006..ddd05ea13f1f4a9231ed88bda098b4a517116841 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>`."