content: {-# LANGUAGE TypeOperators, DataKinds, TypeFamilies #-}
  
  -- | This module exports a dummy test to force type checking of this
  -- module. In this module we test the subtyping system.
  
  module Data.Comp.Subsume_Test where
  
  import Data.Comp
  import Data.Comp.Ops
  import Data.Comp.SubsumeCommon
  
  
  import Test.Framework
  import Test.Framework.Providers.QuickCheck2
  
  
  data S1 a = S1 a
  data S2 a = S2 a
  data S3 a = S3 a
  data S4 a = S4 a
  
  type TA = S1 :+: S2
  type TB = S3 :+: S4
  type T1 = TA :+: TB
  type T2 = TB :+: TA
  type T3 = S2 :+: TB
  
  test1 :: ComprEmb (Elem T1 T1) ~ (Found Here) => Int
  test1 = 1
  
  test2 :: ComprEmb (Elem T1 T2) ~ (Found (Sum (Ri Here) (Le Here))) => Int
  test2 = 1
  
  test3 :: ComprEmb (Elem (T1 :+: S1) T2) ~ Ambiguous => Int
  test3 = 1
  
  test4 :: ComprEmb (Elem T1 (T2 :+: S1)) ~ Ambiguous => Int
  test4 = 1
  
  test5 :: ComprEmb (Elem T1 T3) ~ NotFound => Int
  test5 = 1
  
  test6 :: ComprEmb (Elem TB T1) ~ (Found (Ri Here)) => Int
  test6 = 1
  
  test7 :: ComprEmb (Elem T3 T1) ~ (Found (Sum (Le (Ri Here))(Ri Here))) => Int
  test7 = 1
  
  main = defaultMain [tests]
  
  tests = testGroup "Subsume" [
           testProperty "prop_typecheck" prop_typecheck
          ]
  
  -- dummy test
  prop_typecheck = True
  