tcError

[1 of 2] Compiling Data.Type.Set    ( src/Data/Type/Set.hs, /Users/alice/Downloads/type-level-sets-master/dist-newstyle/build/x86_64-osx/ghc-8.5.20180429/type-level-sets-0.8.8.0/build/Data/Type/Set.o )

src/Data/Type/Set.hs:95:33: error:
    • Could not deduce: ((e : s) :\ x) ~ (e : (s :\ x))
      from the context: (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x)
        bound by the instance declaration
        at src/Data/Type/Set.hs:(93,31)-(94,27)
      or from: (k ~ *, (y : xs :: [k]) ~~ (e : s :: [*]))
        bound by a pattern with constructor:
                   Ext :: forall e (s :: [*]). e -> Set s -> Set (e : s),
                 in an equation for ‘remove’
        at src/Data/Type/Set.hs:95:11-18
      Expected type: Set ((y : xs) :\ x)
        Actual type: Set (e : (s :\ x))
    • In the expression: Ext y (remove xs x)
      In an equation for ‘remove’:
          remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)
      In the instance declaration for ‘Remove (y : xs) x’
    • Relevant bindings include
        x :: Proxy x (bound at src/Data/Type/Set.hs:95:22)
        xs :: Set s (bound at src/Data/Type/Set.hs:95:17)
        y :: e (bound at src/Data/Type/Set.hs:95:15)
        remove :: Set (y : xs) -> Proxy x -> Set ((y : xs) :\ x)
          (bound at src/Data/Type/Set.hs:95:3)
   |
95 |   remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)
   |                                 ^^^^^^^^^^^^^^^^^^^

src/Data/Type/Set.hs:142:29: error:
    • Could not deduce: Nub (e1 : f : s) ~ (e1 : Nub (f : s))
      from the context: (Nub (e : f : s) ~ (e : Nub (f : s)),
                         Nubable (f : s))
        bound by the instance declaration
        at src/Data/Type/Set.hs:(140,27)-(141,56)
      or from: (k ~ *, (e : f : s :: [k]) ~~ (e1 : s1 :: [*]))
        bound by a pattern with constructor:
                   Ext :: forall e (s :: [*]). e -> Set s -> Set (e : s),
                 in an equation for ‘nub’
        at src/Data/Type/Set.hs:142:10-24
      or from: (* ~ *, s1 ~ (e2 : s2))
        bound by a pattern with constructor:
                   Ext :: forall e (s :: [*]). e -> Set s -> Set (e : s),
                 in an equation for ‘nub’
        at src/Data/Type/Set.hs:142:17-23
      Expected type: Set (Nub (e : f : s))
        Actual type: Set (e1 : Nub (f : s))
    • In the expression: Ext e (nub (Ext f s))
      In an equation for ‘nub’:
          nub (Ext e (Ext f s)) = Ext e (nub (Ext f s))
      In the instance declaration for ‘Nubable (e : f : s)’
    • Relevant bindings include
        e :: e1 (bound at src/Data/Type/Set.hs:142:14)
        nub :: Set (e : f : s) -> Set (Nub (e : f : s))
          (bound at src/Data/Type/Set.hs:142:5)
    |
142 |     nub (Ext e (Ext f s)) = Ext e (nub (Ext f s))
    |                             ^^^^^^^^^^^^^^^^^^^^^