diff options
| -rw-r--r-- | compiler/types/CoAxiom.hs | 27 |
1 files changed, 13 insertions, 14 deletions
diff --git a/compiler/types/CoAxiom.hs b/compiler/types/CoAxiom.hs index cd8607a4bb..9a85185cc6 100644 --- a/compiler/types/CoAxiom.hs +++ b/compiler/types/CoAxiom.hs @@ -1,12 +1,12 @@ -- (c) The University of Glasgow 2012 -{-# LANGUAGE CPP, DeriveDataTypeable, GADTs, ScopedTypeVariables #-} +{-# LANGUAGE CPP, DataKinds, DeriveDataTypeable, GADTs, KindSignatures, ScopedTypeVariables, StandaloneDeriving #-} -- | Module for coercion axioms, used to represent type family instances -- and newtypes module CoAxiom ( - Branched, Unbranched, BranchIndex, BranchList(..), + BranchFlag, Branched, Unbranched, BranchIndex, BranchList(..), toBranchList, fromBranchList, toBranchedList, toUnbranchedList, brListLength, brListNth, brListMap, brListFoldr, brListMapM, @@ -108,13 +108,6 @@ declaring whether it is known to be a singleton or not. The list of branches is stored using a special form of list, declared below, that ensures that the type variable is accurate. -As of this writing (Dec 2012), it would not be appropriate to use a promoted -type as the phantom type, so we use empty datatypes. We wish to have GHC -remain compilable with GHC 7.2.1. If you are revising this code and GHC no -longer needs to remain compatible with GHC 7.2.x, then please update this -code to use promoted types. - - ************************************************************************ * * Branch lists @@ -125,11 +118,17 @@ code to use promoted types. type BranchIndex = Int -- The index of the branch in the list of branches -- Counting from zero --- the phantom type labels -data Unbranched deriving Typeable -data Branched deriving Typeable - -data BranchList a br where +-- promoted data type +data BranchFlag = Branched | Unbranched +type Branched = 'Branched +deriving instance Typeable 'Branched +type Unbranched = 'Unbranched +deriving instance Typeable 'Unbranched +-- By using type synonyms for the promoted constructors, we avoid needing +-- DataKinds and the promotion quote in client modules. This also means that +-- we don't need to export the term-level constructors, which should never be used. + +data BranchList a (br :: BranchFlag) where FirstBranch :: a -> BranchList a br NextBranch :: a -> BranchList a br -> BranchList a Branched |