Commit 37227d34 authored by Gabor Greif's avatar Gabor Greif 💬

Make BranchFlag a new kind

this is resolving an old TODO comment
parent d9b618ff
-- (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
......
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