Commit fbd6de2f authored by Jan Stolarek's avatar Jan Stolarek Committed by Ben Gamari
Browse files

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
parent 5cb236dd
......@@ -240,7 +240,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
......@@ -3208,6 +3208,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,
......@@ -3347,6 +3348,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!
......
......@@ -831,7 +831,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
......
......@@ -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
......
......@@ -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>`__.
......
......@@ -45,6 +45,7 @@ data Extension
| UnboxedTuples
| BangPatterns
| TypeFamilies
| InjectiveTypeFamilies
| TypeInType
| OverloadedStrings
| OverloadedLists
......
{-# 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
T11381.hs:7:23:
Illegal injectivity annotation
Use InjectiveTypeFamilies to allow this
In the type family declaration for ‘F’
......@@ -38,7 +38,8 @@ check title expected got
expectedGhcOnlyExtensions :: [String]
expectedGhcOnlyExtensions = ["RelaxedLayout",
"AlternativeLayoutRule",
"AlternativeLayoutRuleTransitional"]
"AlternativeLayoutRuleTransitional",
"InjectiveTypeFamilies"]
expectedCabalOnlyExtensions :: [String]
expectedCabalOnlyExtensions = ["Generics",
......
......@@ -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, [''])
:set -XTypeFamilies
:set -XInjectiveTypeFamilies
:set -XDataKinds
:set -XUndecidableInstances
:set -XPolyKinds
......
:set -XTypeFamilies
:set -XInjectiveTypeFamilies
:set -XDataKinds
:set -XUndecidableInstances
:set -XPolyKinds
......
:set -XTypeFamilies
:set -XInjectiveTypeFamilies
:set -XDataKinds
:set -XUndecidableInstances
:set -XPolyKinds
......
{-# LANGUAGE TypeFamilies, DataKinds, UndecidableInstances, PolyKinds #-}
{-# LANGUAGE InjectiveTypeFamilies, DataKinds, UndecidableInstances,
PolyKinds #-}
module T6018th where
import Language.Haskell.TH
......
{-# LANGUAGE TemplateHaskell, TypeFamilies, PolyKinds #-}
{-# LANGUAGE TemplateHaskell, InjectiveTypeFamilies, PolyKinds #-}
module T8884 where
......
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE InjectiveTypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
......
{-# LANGUAGE TypeFamilies, PolyKinds #-}
{-# LANGUAGE InjectiveTypeFamilies, PolyKinds #-}
module T6018 where
......
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE InjectiveTypeFamilies #-}
module T6018a where
......
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE InjectiveTypeFamilies #-}
module T10836 where
type family Foo a = r | r -> a where
......
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE InjectiveTypeFamilies #-}
module T6018Afail where
......
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE InjectiveTypeFamilies #-}
module T6018Bfail where
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment