Fix #11716.
authorRichard Eisenberg <eir@cis.upenn.edu>
Wed, 16 Mar 2016 19:20:32 +0000 (15:20 -0400)
committerRichard Eisenberg <eir@cis.upenn.edu>
Thu, 17 Mar 2016 14:07:22 +0000 (10:07 -0400)
There were several smallish bugs here:
 - We had too small an InScopeSet when rejigging GADT return types.
 - When adding the extra_tvs with a datatype kind signature, we
   were sometimes changing Uniques of an explicitly bound kind var.
 - Using coercionKind in the flattener got the wrong visibility
   for a binder. Now we just zonk to get what we need.

Test case: dependent/should_compile/RaeJobTalk

compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcFlatten.hs
compiler/typecheck/TcHsType.hs
compiler/typecheck/TcPat.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcType.hs
testsuite/tests/dependent/should_compile/RaeJobTalk.hs [new file with mode: 0644]
testsuite/tests/dependent/should_compile/all.T

index a5fd412..db69e7b 100644 (file)
@@ -559,7 +559,7 @@ can_eq_nc' flat _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
 -- Check only when flat because the zonk_eq_types check in canEqNC takes
 -- care of the non-flat case.
 can_eq_nc' True _rdr_env _envs ev ReprEq ty1 _ ty2 _
-  | ty1 `eqType` ty2
+  | ty1 `tcEqType` ty2
   = canEqReflexive ev ReprEq ty1
 
 -- When working with ReprEq, unwrap newtypes.
@@ -1505,7 +1505,7 @@ homogeniseRhsKind :: CtEvidence -- ^ the evidence to homogenise
                            -- the 'Xi' is the new RHS
                   -> TcS (StopOrContinue Ct)
 homogeniseRhsKind ev eq_rel lhs rhs build_ct
-  | k1 `eqType` k2
+  | k1 `tcEqType` k2
   = continueWith (build_ct ev rhs)
 
   | CtGiven { ctev_evar = evar } <- ev
index 169232e..491888e 100644 (file)
@@ -1344,8 +1344,8 @@ flatten_tyvar3 tv
 --           (vcat [ ppr tv <+> dcolon <+> ppr (tyVarKind tv)
 --                 , ppr _new_kind
 --                 , ppr kind_co <+> dcolon <+> ppr (coercionKind kind_co) ])
-       ; let Pair _ orig_kind = coercionKind kind_co
-             -- orig_kind might be zonked
+       ; orig_kind <- liftTcS $ zonkTcType kind
+             -- NB: orig_kind is *not* the kind returned from flatten
        ; return (FTRCasted (setTyVarKind tv orig_kind) kind_co) }
 
 {-
index 37a8675..552c0d0 100644 (file)
@@ -1842,12 +1842,18 @@ tcDataKindSig kind
                             , isNothing (lookupLocalRdrOcc rdr_env occ) ]
                  -- Note [Avoid name clashes for associated data types]
 
-        ; return ( [ mk_tv span uniq occ kind
-                   | ((kind, occ), uniq) <- arg_kinds `zip` occs `zip` uniqs ]
+            -- NB: Use the tv from a binder if there is one. Otherwise,
+            -- we end up inventing a new Unique for it, and any other tv
+            -- that mentions the first ends up with the wrong kind.
+        ; return ( [ tv
+                   | ((bndr, occ), uniq) <- bndrs `zip` occs `zip` uniqs
+                   , let tv | Just bndr_tv <- binderVar_maybe bndr
+                            = bndr_tv
+                            | otherwise
+                            = mk_tv span uniq occ (binderType bndr) ]
                  , bndrs, res_kind ) }
   where
     (bndrs, res_kind) = splitPiTys kind
-    arg_kinds         = map binderType bndrs
     mk_tv loc uniq occ kind
       = mkTyVar (mkInternalName uniq occ loc) kind
 
index ae3c202..53b8142 100644 (file)
@@ -747,9 +747,14 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty arg_pats thing_inside
 
               arg_tys' = substTys tenv arg_tys
 
-        ; traceTc "tcConPat" (vcat [ ppr con_name, ppr univ_tvs, ppr ex_tvs
+        ; traceTc "tcConPat" (vcat [ ppr con_name
+                                   , pprTvBndrs univ_tvs
+                                   , pprTvBndrs ex_tvs
                                    , ppr eq_spec
-                                   , ppr ex_tvs', ppr ctxt_res_tys, ppr arg_tys'
+                                   , ppr theta
+                                   , pprTvBndrs ex_tvs'
+                                   , ppr ctxt_res_tys
+                                   , ppr arg_tys'
                                    , ppr arg_pats ])
         ; if null ex_tvs && null eq_spec && null theta
           then do { -- The common case; no class bindings etc
index cfd9559..8fa967d 100644 (file)
@@ -1823,6 +1823,7 @@ mkGADTVars tmpl_tvs dc_tvs subst
   = choose [] [] empty_subst empty_subst tmpl_tvs
   where
     in_scope = mkInScopeSet (mkVarSet tmpl_tvs `unionVarSet` mkVarSet dc_tvs)
+               `unionInScope` getTCvInScope subst
     empty_subst = mkEmptyTCvSubst in_scope
 
     choose :: [TyVar]           -- accumulator of univ tvs, reversed
@@ -1844,12 +1845,12 @@ mkGADTVars tmpl_tvs dc_tvs subst
             ,  tyVarKind r_tv `eqType` (substTy t_sub (tyVarKind t_tv))
             -> -- simple, well-kinded variable substitution.
                choose (r_tv:univs) eqs
-                      (extendTvSubst t_sub t_tv r_ty)
-                      (extendTvSubst r_sub r_tv r_ty)
+                      (extendTvSubst t_sub t_tv r_ty')
+                      (extendTvSubst r_sub r_tv r_ty')
                       t_tvs
             where
               r_tv1  = setTyVarName r_tv (choose_tv_name r_tv t_tv)
-              r_ty   = mkTyVarTy r_tv1
+              r_ty'  = mkTyVarTy r_tv1
 
                -- not a simple substitution. make an equality predicate
           _ -> choose (t_tv':univs) (mkEqSpec t_tv' r_ty : eqs)
index a9ea60b..5b37a00 100644 (file)
@@ -180,6 +180,7 @@ module TcType (
   pprKind, pprParendKind, pprSigmaType,
   pprType, pprParendType, pprTypeApp, pprTyThingCategory,
   pprTheta, pprThetaArrowTy, pprClassPred,
+  pprTvBndr, pprTvBndrs,
 
   TypeSize, sizeType, sizeTypes, toposortTyVars
 
diff --git a/testsuite/tests/dependent/should_compile/RaeJobTalk.hs b/testsuite/tests/dependent/should_compile/RaeJobTalk.hs
new file mode 100644 (file)
index 0000000..705c0ef
--- /dev/null
@@ -0,0 +1,697 @@
+{- Copyright (c) 2016 Richard Eisenberg
+ -}
+
+{-# LANGUAGE TypeOperators, TypeFamilies, TypeApplications,
+             ExplicitForAll, ScopedTypeVariables, GADTs, TypeFamilyDependencies,
+             TypeInType, ConstraintKinds, UndecidableInstances,
+             FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies,
+             FlexibleContexts, StandaloneDeriving, InstanceSigs,
+             RankNTypes, UndecidableSuperClasses #-}
+
+module RaeJobTalk where
+
+import Data.Type.Bool
+import Data.Type.Equality
+import GHC.TypeLits
+import Data.Proxy
+import GHC.Exts
+import Data.Kind
+import Unsafe.Coerce
+import Data.Char
+import Data.Maybe
+
+-------------------------------
+-- Utilities
+
+-- Heterogeneous propositional equality
+data (a :: k1) :~~: (b :: k2) where
+  HRefl :: a :~~: a
+
+-- Type-level inequality
+type a /= b = Not (a == b)
+
+-- append type-level lists (schemas)
+type family s1 ++ s2 where
+  '[]       ++ s2 = s2
+  (s ': s1) ++ s2 = s ': (s1 ++ s2)
+
+-- This is needed in order to prove disjointness, because GHC can't
+-- handle inequality well.
+assumeEquality :: forall a b r. ((a ~ b) => r) -> r
+assumeEquality thing = case unsafeCoerce Refl :: a :~: b of
+  Refl -> thing
+
+-- Shorter name for shorter example
+eq :: TestEquality f => f a -> f b -> Maybe (a :~: b)
+eq = testEquality
+
+-------------------------------
+-- Singleton lists
+
+-- Unlike in the singletons paper, we now have injective type
+-- families, so we use that to model singletons; it's a bit
+-- cleaner than the original approach
+type family Sing = (r :: k -> Type) | r -> k
+
+-- Cute type synonym.
+type Π = Sing
+
+-- Really, just singleton lists. Named Schema for better output
+-- during example.
+data Schema :: forall k. [k] -> Type where
+  Nil :: Schema '[]
+  (:>>) :: Sing h -> Schema t -> Schema (h ': t)
+infixr 5 :>>
+type instance Sing = Schema
+
+-- Append singleton lists
+(%:++) :: Schema a -> Schema b -> Schema (a ++ b)
+Nil %:++ x = x
+(a :>> b) %:++ c = a :>> (b %:++ c)
+
+--------------------------------
+-- Type-indexed type representations
+-- Based on "A reflection on types"
+
+data TyCon (a :: k) where
+  Int :: TyCon Int
+  Bool :: TyCon Bool
+  Char :: TyCon Char
+  List :: TyCon []
+  Maybe :: TyCon Maybe
+  Arrow :: TyCon (->)
+  TYPE  :: TyCon TYPE
+  RuntimeRep :: TyCon RuntimeRep
+  PtrRepLifted' :: TyCon 'PtrRepLifted
+  -- If extending, add to eqTyCon too
+
+eqTyCon :: TyCon a -> TyCon b -> Maybe (a :~~: b)
+eqTyCon Int Int = Just HRefl
+eqTyCon Bool Bool = Just HRefl
+eqTyCon Char Char = Just HRefl
+eqTyCon List List = Just HRefl
+eqTyCon Maybe Maybe = Just HRefl
+eqTyCon Arrow Arrow = Just HRefl
+eqTyCon TYPE TYPE = Just HRefl
+eqTyCon RuntimeRep RuntimeRep = Just HRefl
+eqTyCon PtrRepLifted' PtrRepLifted' = Just HRefl
+eqTyCon _ _ = Nothing
+
+-- Check whether or not a type is really a plain old tycon;
+-- necessary to avoid warning in kindRep
+type family Primitive (a :: k) :: Constraint where
+  Primitive (_ _) = ('False ~ 'True)
+  Primitive _     = (() :: Constraint)
+
+data TypeRep (a :: k) where
+  TyCon :: forall (a :: k). (Primitive a, Typeable k) => TyCon a -> TypeRep a
+  TyApp :: TypeRep a -> TypeRep b -> TypeRep (a b)
+
+-- Equality on TypeReps
+eqT :: TypeRep a -> TypeRep b -> Maybe (a :~~: b)
+eqT (TyCon tc1) (TyCon tc2) = eqTyCon tc1 tc2
+eqT (TyApp f1 a1) (TyApp f2 a2) = do
+  HRefl <- eqT f1 f2
+  HRefl <- eqT a1 a2
+  return HRefl
+eqT _ _ = Nothing
+
+
+--------------------------------------
+-- Existentials
+
+data TyConX where
+  TyConX :: forall (a :: k). (Primitive a, Typeable k) => TyCon a -> TyConX
+
+instance Read TyConX where
+  readsPrec _ "Int" = [(TyConX Int, "")]
+  readsPrec _ "Bool" = [(TyConX Bool, "")]
+  readsPrec _ "List" = [(TyConX List, "")]
+  readsPrec _ _ = []
+
+-- This variant of TypeRepX allows you to specify an arbitrary
+-- constraint on the inner TypeRep
+data TypeRepX :: (forall k. k -> Constraint) -> Type where
+  TypeRepX :: forall k (c :: forall k'. k' -> Constraint) (a :: k).
+              c a => TypeRep a -> TypeRepX c
+
+-- This constraint is always satisfied
+class ConstTrue (a :: k) -- needs the :: k to make it a specified tyvar
+instance ConstTrue a
+
+instance Show (TypeRepX ConstTrue) where
+  show (TypeRepX tr) = show tr
+
+-- can't write Show (TypeRepX c) because c's kind mentions a forall,
+-- and the impredicativity check gets nervous. See #11519
+instance Show (TypeRepX IsType) where
+  show (TypeRepX tr) = show tr
+
+-- Just enough functionality to get through example. No parentheses
+-- or other niceties.
+instance Read (TypeRepX ConstTrue) where
+  readsPrec p s = do
+    let tokens = words s
+    tyreps <- mapM read_token tokens
+    return (foldl1 mk_app tyreps, "")
+
+    where
+      read_token :: String -> [TypeRepX ConstTrue]
+      read_token "String" = return (TypeRepX $ typeRep @String)
+      read_token other = do
+        (TyConX tc, _) <- readsPrec p other
+        return (TypeRepX (TyCon tc))
+
+      mk_app :: TypeRepX ConstTrue -> TypeRepX ConstTrue -> TypeRepX ConstTrue
+      mk_app (TypeRepX f) (TypeRepX a) = case kindRep f of
+        TyCon Arrow `TyApp` k1 `TyApp` _
+          | Just HRefl <- k1 `eqT` kindRep a -> TypeRepX (TyApp f a)
+        _ -> error "ill-kinded type"
+
+-- instance Read (TypeRepX ((~~) Type))  RAE: need (~~) :: forall k1. k1 -> forall k2. k2 -> Constraint
+-- RAE: need kind signatures on classes
+
+-- TypeRepX ((~~) Type)
+-- (~~) :: forall k1 k2. k1 -> k2 -> Constraint
+-- I need: (~~) :: forall k1. k1 -> forall k2. k2 -> Constraint
+
+class k ~~ Type => IsType (x :: k)
+instance k ~~ Type => IsType (x :: k)
+
+instance Read (TypeRepX IsType) where
+  readsPrec p s = case readsPrec @(TypeRepX ConstTrue) p s of
+    [(TypeRepX tr, "")]
+      | Just HRefl <- eqT (kindRep tr) (typeRep @Type)
+      -> [(TypeRepX tr, "")]
+    _ -> error "wrong kind"
+
+-----------------------------
+-- Get the kind of a type
+
+kindRep :: TypeRep (a :: k) -> TypeRep k
+kindRep (TyCon _) = typeRep
+kindRep (TyApp (f :: TypeRep (tf :: k1 -> k)) _) = case kindRep f :: TypeRep (k1 -> k) of
+  TyApp _ res -> res
+
+-- Convert an explicit TypeRep into an implicit one. Doesn't require unsafeCoerce
+-- in Core
+withTypeable :: forall a r. TypeRep a -> (Typeable a => r) -> r
+withTypeable tr thing = unsafeCoerce (Don'tInstantiate thing :: DI a r) tr
+newtype DI a r = Don'tInstantiate (Typeable a => r)
+
+-----------------------------
+-- Implicit TypeReps (Typeable)
+
+class (Primitive a, Typeable k) => TyConAble (a :: k) where
+  tyCon :: TyCon a
+
+instance TyConAble Int       where tyCon = Int
+instance TyConAble Bool      where tyCon = Bool
+instance TyConAble Char      where tyCon = Char
+instance TyConAble []        where tyCon = List
+instance TyConAble Maybe     where tyCon = Maybe
+instance TyConAble (->)      where tyCon = Arrow
+instance TyConAble TYPE      where tyCon = TYPE
+instance TyConAble 'PtrRepLifted   where tyCon = PtrRepLifted'
+instance TyConAble RuntimeRep    where tyCon = RuntimeRep
+
+-- Can't just define Typeable the way we want, because the instances
+-- overlap. So we have to mock up instance chains via closed type families.
+class Typeable' (a :: k) (b :: Bool) where
+  typeRep' :: TypeRep a
+
+type family CheckPrim a where
+  CheckPrim (_ _) = 'False
+  CheckPrim _     = 'True
+
+-- NB: We need the ::k and the ::Constraint so that this has a CUSK, allowing
+-- the polymorphic recursion with TypeRep. See also #9200, though the requirement
+-- for the constraints is correct.
+type Typeable (a :: k) = (Typeable' a (CheckPrim a) :: Constraint)
+
+instance TyConAble a => Typeable' a 'True where
+  typeRep' = TyCon tyCon
+
+instance (Typeable a, Typeable b) => Typeable' (a b) 'False where
+  typeRep' = TyApp typeRep typeRep
+
+typeRep :: forall a. Typeable a => TypeRep a
+typeRep = typeRep' @_ @_ @(CheckPrim a) -- RAE: #11512 says we need the extra @_.
+
+-----------------------------
+-- Useful instances
+
+instance Show (TypeRep a) where
+  show (TyCon tc) = show tc
+  show (TyApp tr1 tr2) = show tr1 ++ " " ++ show tr2
+
+deriving instance Show (TyCon a)
+
+instance TestEquality TypeRep where
+  testEquality tr1 tr2
+    | Just HRefl <- eqT tr1 tr2
+    = Just Refl
+    | otherwise
+    = Nothing
+
+---------------------------
+-- More singletons
+
+-- a TypeRep really is a singleton
+type instance Sing = (TypeRep :: Type -> Type)
+
+data SSymbol :: Symbol -> Type where
+  SSym :: KnownSymbol s => SSymbol s
+type instance Sing = SSymbol
+
+instance TestEquality SSymbol where
+  testEquality :: forall s1 s2. SSymbol s1 -> SSymbol s2 -> Maybe (s1 :~: s2)
+  testEquality SSym SSym = sameSymbol @s1 @s2 Proxy Proxy
+
+instance Show (SSymbol name) where
+  show s@SSym = symbolVal s
+
+
+--------------
+-- Finds Read and Show instances for the example
+getReadShowInstances :: TypeRep a
+                     -> ((Show a, Read a) => r)
+                     -> r
+getReadShowInstances tr thing
+  | Just HRefl <- eqT tr (typeRep @Int) = thing
+  | Just HRefl <- eqT tr (typeRep @Bool) = thing
+  | Just HRefl <- eqT tr (typeRep @Char) = thing
+
+  | TyApp list_rep elt_rep <- tr
+  , Just HRefl <- eqT list_rep (typeRep @[])
+  = getReadShowInstances elt_rep $ thing
+
+  | otherwise = error $ "I don't know how to read or show " ++ show tr
+
+-------------------------
+-- A named column in our database
+data Column = Attr Symbol Type
+type Col = 'Attr
+
+-- Singleton for columns
+data SColumn :: Column -> Type where
+  Col :: Sing s -> TypeRep ty -> SColumn (Col s ty)
+type instance Sing = SColumn
+
+-- Extract the type of a column
+type family ColType col where
+  ColType (Col _ ty) = ty
+
+-- A schema is an ordered list of named attributes
+type TSchema = [Column]
+
+-- predicate to check that a schema is free of a certain attribute
+type family ColNotIn name s where
+  ColNotIn _    '[]                    = 'True
+  ColNotIn name ((Col name' _) ': t) =
+    (name /= name') && (ColNotIn name t)
+
+-- predicate to check that two schemas are disjoint
+type family Disjoint s1 s2 where
+  Disjoint '[]      _ = 'True
+  Disjoint ((Col name ty) ': t) s = (ColNotIn name s) && (Disjoint t s)
+
+-- A Row is one row of our database table, keyed by its schema.
+data Row :: TSchema -> Type where
+  EmptyRow :: Row '[]
+  (::>) :: ColType col -> Row s -> Row (col ': s)
+infixr 5 ::>
+
+-- Map a predicate over all the types in a schema
+type family AllSchemaTys c sch where
+  AllSchemaTys _ '[] = (() :: Constraint)
+  AllSchemaTys c (col ': cols) = (c (ColType col), AllSchemaTys c cols)
+
+-- Convenient abbreviations for being to print and parse the types
+-- in a schema
+type ShowSchema s = AllSchemaTys Show s
+type ReadSchema s = AllSchemaTys Read s
+
+-- We can easily print out rows, as long as the data are printable
+instance ShowSchema s => Show (Row s) where
+  show EmptyRow  = ""
+  show (h ::> t) = show h ++ " " ++ show t
+
+-- In our simplistic case, we just store the list of rows. A more
+-- sophisticated implementation could store some identifier to the connection
+-- to an external database.
+data Table :: TSchema -> Type where
+  Table :: [Row s] -> Table s
+
+instance ShowSchema s => Show (Table s) where
+  show (Table rows) = unlines (map show rows)
+
+-- The following functions parse our very simple flat file database format.
+
+-- The file, with a name ending in ".table", consists of a sequence of lines,
+-- where each line contains one entry in the table. There is no row separator;
+-- if a row contains n pieces of data, that row is represented in n lines in
+-- the file.
+
+-- A schema is stored in a file ending in ".schema".
+-- Each line is a column name followed by its type.
+
+-- Read a row of a table
+readRow :: ReadSchema s => Schema s -> [String] -> (Row s, [String])
+readRow Nil             strs    = (EmptyRow, strs)
+readRow (_ :>> _)       []      = error "Ran out of data while processing row"
+readRow (_ :>> schTail) (sh:st) = (read sh ::> rowTail, strTail)
+  where (rowTail, strTail) = readRow schTail st
+
+-- Read in a table
+readRows :: ReadSchema s => Schema s -> [String] -> [Row s]
+readRows _   []  = []
+readRows sch lst = (row : tail)
+  where (row, strTail) = readRow  sch lst
+        tail           = readRows sch strTail
+
+-- Read in one line of a .schema file. Note that the type read must have kind *
+readCol :: String -> (String, TypeRepX IsType)
+readCol str = case break isSpace str of
+  (name, ' ' : ty) -> (name, read ty)
+  _                -> schemaError $ "Bad parse of " ++ str
+
+-- Load in a schema.
+withSchema :: String
+           -> (forall (s :: TSchema). Schema s -> IO a)
+           -> IO a
+withSchema filename thing_inside = do
+  schString <- readFile filename
+  let schEntries = lines schString
+      cols       = map readCol schEntries
+  go cols thing_inside
+  where
+    go :: [(String, TypeRepX IsType)]
+       -> (forall (s :: TSchema). Schema s -> IO a)
+       -> IO a
+    go []                           thing = thing Nil
+    go ((name, TypeRepX tr) : cols) thing
+      = go cols $ \schema ->
+        case someSymbolVal name of
+          SomeSymbol (_ :: Proxy name) ->
+            thing (Col (SSym @name) tr :>> schema)
+
+-- Load in a table of a given schema
+loadTable :: ReadSchema s => String -> Schema s -> IO (Table s)
+loadTable name schema = do
+  dataString <- readFile name
+  return (Table $ readRows schema (lines dataString))
+
+-- In order to define strongly-typed projection from a row, we need to have a notion
+-- that one schema is a subset of another. We permit the schemas to have their columns
+-- in different orders. We define this subset relation via two inductively defined
+-- propositions. In Haskell, these inductively defined propositions take the form of
+-- GADTs. In their original form, they would look like this:
+{-
+data InProof :: Column -> Schema -> * where
+  InHere  :: InProof col (col ': schTail)
+  InThere :: InProof col cols -> InProof col (a ': cols)
+
+data SubsetProof :: Schema -> Schema -> * where
+  SubsetEmpty :: SubsetProof '[] s'
+  SubsetCons  :: InProof col s' -> SubsetProof cols s'
+              -> SubsetProof (col ': cols) s'
+-}
+-- However, it would be convenient to users of the database library not to require
+-- building these proofs manually. So, we define type classes so that the compiler
+-- builds the proofs automatically. To make everything work well together, we also
+-- make the parameters to the proof GADT constructors implicit -- i.e. in the form
+-- of type class constraints.
+
+data InProof :: Column -> TSchema -> Type where
+  InHere  :: InProof col (col ': schTail)
+  InThere :: In name u cols => InProof (Col name u) (a ': cols)
+
+class In (name :: Symbol) (u :: Type) (sch :: TSchema) where
+  inProof :: InProof (Col name u) sch
+
+-- These instances must be INCOHERENT because they overlap badly. The coherence
+-- derives from the fact that one schema will mention a name only once, but this
+-- is beyond our capabilities to easily encode, given the lack of a solver for
+-- type-level finite maps.
+instance {-# INCOHERENT #-} In name u ((Col name u) ': schTail) where
+  inProof = InHere
+instance {-# INCOHERENT #-} In name u cols => In name u (a ': cols) where
+  inProof = InThere
+
+data SubsetProof :: TSchema -> TSchema -> Type where
+  SubsetEmpty :: SubsetProof '[] s'
+  SubsetCons :: (In name u s', Subset cols s')
+             => Proxy name -> Proxy u -> SubsetProof ((Col name u) ': cols) s'
+
+class SubsetSupport s s' => Subset (s :: TSchema) (s' :: TSchema) where
+  subset :: SubsetProof s s'
+
+  -- The use of this constraint family allows us to assume a subset relationship
+  -- when we recur on the structure of s.
+  type SubsetSupport s s' :: Constraint
+
+instance Subset '[] s' where
+  subset = SubsetEmpty
+  type SubsetSupport '[] s' = ()
+
+instance (In name u s', Subset cols s') =>
+           Subset ((Col name u) ': cols) s' where
+  subset = SubsetCons Proxy Proxy
+  type SubsetSupport ((Col name u) ': cols) s' = Subset cols s'
+
+-- To access the data in a structured (and well-typed!) way, we use
+-- an RA (short for Relational Algebra). An RA is indexed by the schema
+-- of the data it produces.
+
+data RA :: TSchema -> Type where
+  -- The RA includes all data represented by the handle.
+  Read :: Table s -> RA s
+
+  -- The RA is a Cartesian product of the two RAs provided. Note that
+  -- the schemas of the two provided RAs must be disjoint.
+  Product :: (Disjoint s s' ~ 'True) => RA s -> RA s' -> RA (s ++ s')
+
+  -- The RA is a projection conforming to the schema provided. The
+  -- type-checker ensures that this schema is a subset of the data
+  -- included in the provided RA.
+  Project :: Subset s' s => RA s -> RA s'
+
+  -- The RA contains only those rows of the provided RA for which
+  -- the provided expression evaluates to True. Note that the
+  -- schema of the provided RA and the resultant RA are the same
+  -- because the columns of data are the same. Also note that
+  -- the expression must return a Bool for this to type-check.
+  Select :: Expr s Bool -> RA s -> RA s
+
+-- Other constructors would be added in a more robust database
+-- implementation.
+
+-- An Expr is used with the Select constructor to choose some
+-- subset of rows from a table. Expressions are indexed by the
+-- schema over which they operate and the return value they
+-- produce.
+data Expr :: TSchema -> Type -> Type where
+  (:+), (:-), (:*), (:/) :: Expr s Int -> Expr s Int -> Expr s Int
+
+  (:<), (:<=), (:>), (:>=), (:==), (:/=)
+    :: Ord a => Expr s a -> Expr s a -> Expr s Bool
+
+  -- A literal
+  Literal :: ty -> Expr s ty
+
+  -- element of a list
+  ElementOf :: Eq ty => Expr s ty -> Expr s [ty] -> Expr s Bool
+
+  -- Projection in an expression -- evaluates to the value
+  -- of the named column.
+  Element :: In name ty s => Proxy name -> Expr s ty
+
+-- Choose the elements of one list based on truth values in another
+choose :: [Bool] -> [a] -> [a]
+choose bs as = [ a | (a,True) <- zip as bs ]
+
+-- Project a component of one row, assuming that the desired projection
+-- is valid.
+projectRow :: forall sub super.
+              Subset sub super => Row super -> Row sub
+projectRow r = case subset @sub @super of
+  SubsetEmpty -> EmptyRow
+  SubsetCons (_ :: Proxy name) (_ :: Proxy ty) ->
+      find_datum inProof r ::> projectRow r
+    where
+      find_datum :: InProof (Col name ty) s -> Row s -> ty
+      find_datum InHere  (h ::> _) = h
+      find_datum InThere (_ ::> t) = find_datum inProof t
+
+-- Evaluate an Expr
+eval :: Expr s ty -> Row s -> ty
+eval (a :+ b)  r = eval a r +  eval b r
+eval (a :- b)  r = eval a r -  eval b r
+eval (a :* b)  r = eval a r *  eval b r
+eval (a :/ b)  r = eval a r `div` eval b r
+eval (a :< b)  r = eval a r <  eval b r
+eval (a :<= b) r = eval a r <= eval b r
+eval (a :> b)  r = eval a r >  eval b r
+eval (a :>= b) r = eval a r >= eval b r
+eval (a :== b) r = eval a r == eval b r
+eval (a :/= b) r = eval a r /= eval b r
+eval (Literal n)                 _ = n
+eval (ElementOf elt list)        r = eval elt r `elem` eval list r
+eval (Element (_ :: Proxy name)) r = get_element inProof r
+  where
+    get_element :: InProof (Col name ty) s -> Row s -> ty
+    get_element InHere (elt ::> _) = elt
+    get_element InThere (_ ::> tail) = get_element inProof tail
+
+-- Append two rows. Needed for Cartesian product.
+rowAppend :: Row s -> Row s' -> Row (s ++ s')
+rowAppend EmptyRow  r = r
+rowAppend (h ::> t) r = h ::> rowAppend t r
+
+-- The query function is the eliminator for an RA. It returns a list of
+-- rows containing the data produced by the RA. In the IO monad only
+-- because more sophisticated implementations would actually go out to
+-- a DB server for this.
+query :: RA s -> IO [Row s]
+query (Read (Table rows)) = return rows
+query (Product ra rb) = do
+  rowsa <- query ra
+  rowsb <- query rb
+  return [ rowAppend rowa rowb | rowa <- rowsa, rowb <- rowsb ]
+query (Project ra)     = map projectRow <$> query ra
+query (Select expr ra) = filter (eval expr) <$> query ra
+
+field :: forall name ty s. In name ty s => Expr s ty
+field = Element (Proxy :: Proxy name)
+
+
+
+
+
+
+
+
+-- A schema is a list of columns, with
+-- data Column = Col String Type
+-- NB: Dependent type support is still experimental
+checkIn :: Π name -> Π ty -> Π schema
+        -> (In name ty schema => r)
+        -> r
+checkIn name _  Nil                        _
+  = schemaError ("Field " ++ show name ++ " not found.")
+checkIn name ty ((Col name' ty') :>> rest) callback
+  = case (name `eq` name', ty `eq` ty') of
+      (Just Refl, Just Refl) -> callback
+      (Just _,    _)         -> schemaError ("Found " ++ show name ++
+                                             " but it maps to " ++ show ty')
+      _                      -> checkIn name ty rest callback
+
+-- example call:
+-- checkIn "id" Int schema ({- access "id" and assume it has type Int -})
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+-- Establish a Subset constraint
+checkSubset :: Π sch1 -> Π sch2 -> (Subset sch1 sch2 => r) -> r
+checkSubset Nil                    _     callback = callback
+checkSubset (Col name ty :>> rest) super callback
+  = checkSubset rest super $
+    checkIn name ty super $
+    callback
+
+-- Check that two names are distinct
+checkNotEqual :: forall (name1 :: Symbol) name2 r.
+                 Π name1 -> Π name2
+              -> (((name1 /= name2) ~ 'True) => r) -> r
+checkNotEqual name1 name2 callback
+  = case name1 `eq` name2 of
+      Just Refl -> schemaError $ "Found " ++ show name1 ++
+                          " in both supposedly disjoint schemas."
+      Nothing   -> assumeEquality @(name1 /= name2) @'True $
+                   callback
+
+-- Establish a ColNotIn condition
+checkColNotIn :: Π name -> Π sch2
+              -> ((ColNotIn name sch2 ~ 'True) => r) -> r
+checkColNotIn _    Nil                    callback = callback
+checkColNotIn name (Col name' _ :>> rest) callback
+  = checkNotEqual name name' $
+    checkColNotIn name rest $
+    callback
+
+-- Establish a Disjointness constraint
+checkDisjoint :: Π sch1 -> Π sch2
+              -> ((Disjoint sch1 sch2 ~ 'True) => r) -> r
+checkDisjoint Nil                   _    callback = callback
+checkDisjoint (Col name _ :>> rest) sch2 callback
+  = checkColNotIn name sch2 $
+    checkDisjoint rest sch2 $
+    callback
+
+-- Establish a ShowSchema constraint
+checkShowSchema :: Π sch -> (ShowSchema sch => r) -> r
+checkShowSchema Nil                 callback = callback
+checkShowSchema (Col _ ty :>> rest) callback
+  = getReadShowInstances ty $
+    checkShowSchema rest $
+    callback
+
+-- Establish a ReadSchema constraint
+checkReadSchema :: Π sch -> (ReadSchema sch => r) -> r
+checkReadSchema Nil                 callback = callback
+checkReadSchema (Col _ ty :>> rest) callback
+  = getReadShowInstances ty $
+    checkReadSchema rest $
+    callback
+
+-- Terminate program with an easy-to-understand message
+schemaError :: String -> a
+schemaError str = errorWithoutStackTrace $ "Schema validation error: " ++ str
+
+-------------------------
+type NameSchema = [ Col "first" String, Col "last" String ]
+
+printName :: Row NameSchema -> IO ()
+printName (first ::> last ::> _) = putStrLn (first ++ " " ++ last)
+
+readDB classes_sch students_sch = do
+  classes_tab  <- loadTable "classes.table" classes_sch
+  students_tab <- loadTable "students.table" students_sch
+
+  putStr "Whose students do you want to see? "
+  prof <- getLine
+
+  let joined = Project (
+                Select (field @"id" @Int `ElementOf` field @"students") (
+                 Product (Select (field @"prof" :== Literal prof) (Read classes_tab))
+                         (Read students_tab)))
+  rows <- query joined
+  mapM_ printName rows
+
+------------------
+main :: IO ()
+main = withSchema "classes.schema" $ \classes_sch ->
+       withSchema "students.schema" $ \students_sch ->
+       checkDisjoint classes_sch students_sch $
+       checkIn (SSym @"students") (typeRep @[Int]) (classes_sch %:++ students_sch) $
+       checkIn (SSym @"prof") (typeRep @String) classes_sch $
+       checkIn (SSym @"last") (typeRep @String) (classes_sch %:++ students_sch) $
+       checkIn (SSym @"id") (typeRep @Int) (classes_sch %:++ students_sch) $
+       checkIn (SSym @"first") (typeRep @String) (classes_sch %:++ students_sch) $
+       checkReadSchema students_sch $
+       checkReadSchema classes_sch $
+       readDB classes_sch students_sch
index 8ecd105..2f9d311 100644 (file)
@@ -18,3 +18,4 @@ test('T11311', normal, compile, [''])
 test('T11405', normal, compile, [''])
 test('T11241', normal, compile, [''])
 test('T11711', normal, compile, [''])
+test('RaeJobTalk', normal, compile, [''])