liftVariant IsSubset constraint

[fonghou]

Hello, thanks for the very neat library!

x :: V '[Int,String]
x = V @int 1

y :: ('[String,Int] :<< v) => V v
y = liftVariant x

gives a type error

Could not deduce: Haskus.Utils.Types.List.IsSubset '[Int,String] v ~ 'True
  arising from a use of liftVariant
from the context: '[String, Int] :<< v
  bound by the type signature for: 
      y :: forall (v :: [*]). ('[String, Int] :<< v) => V v

Should IsSubset be True here (as subset relation should be reflexive)?

Cheers!

[pcarbonn]

The order of constructors is significant... Try with '[Int,String] everywhere. It is a list, not a set.

Edit: The error message could better say "IsSubList".

[hsyl20]

Yes the order of the constructors matters. Also you have to use the LiftVariant constraint as follows:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}

import Haskus.Utils.Variant

x :: V '[Int,String]
x = V @Int 1

y :: (LiftVariant '[Int,String] v) => V v
y = liftVariant x

-- > y @'[Double,Int,Float,String]
-- V @Int 1

[fonghou]

An example in the doc allows reordering though (only if the output type is concrete?)

x :: V '[Int,String]
x = V @Int 1

-- reordering
y :: V '[String,Int]
y = liftVariant x

@hsyl20 example above actually raises a type error even if the orders are same.

y2 :: (LiftVariant '[Int,String] v) => V v
y2 = liftVariant x

    • Couldn't match type ‘haskus-utils-types-1.1:Haskus.Utils.Types.List.IsSubset
                             '[Int, String] v’
                     with ‘'True’
        arising from a use of ‘liftVariant’
    • In the expression: liftVariant x
      In an equation for ‘y2’: y2 = liftVariant x

The real use case I want to try is based on the recent post on Reddit about Typed Error. However, instead of the solution @hsyl20 posted using RebindableSyntax, I'd like to keep two things:

1. use Either monad so that I can use and compose with mtl instances.
2. use typeclass constraints to allow callee inject its (V err) into caller's (potential larger and reordered) superset (V err).

Here is what I come up with, but only that liftVariant does not type check (btw, change it to liftVariant' (with the tick at the end) does type check, and code runs).

module TypedError (main) where

import Haskus.Utils.ContFlow
import Haskus.Utils.Variant

data FooErr = FooErr Int
    deriving (Show, Generic)

data BarErr = BarErr String
    deriving (Generic, Show)

data BazErr = BazErr String
    deriving (Generic, Show)

foo :: (FooErr :< err) => Either (V err) Int
foo = Left $ V (FooErr 3)

bar :: (BarErr :< err) => Either (V err) Int
bar = Left $ V (BarErr "Hello")

baz :: (BazErr :< err) => Either (V err) Int
baz = Left $ V (BazErr "Oops")

foobarbaz :: ('[FooErr, BarErr, BazErr] :<< err) => Either (V err) Int
foobarbaz = baz *> bar *> foo

foobar :: ('[FooErr, BarErr] :<< err) => Either (V err) Int
foobar = case foobarbaz @'[FooErr, BarErr, BazErr] of
  Right i -> Right i
  Left v -> case popVariant v of
    Right (BazErr _) -> Right 0
    Left leftover    -> Left $ **liftVariant** leftover

-- | And this works!
main :: IO ()
main = do
  print (foo :: Either (V '[FooErr]) Int)
  print (bar @'[BarErr])
  case foobar @'[FooErr,BarErr] of
    Right i -> print i
    Left e  -> variantToCont e >::>
      ( \(FooErr i) -> print i
      , \(BarErr s) -> error ("Found error: " <> s)
      )

[hsyl20]

I'm may be missing something because to make it type-check with liftVariant, I just have to change:

foobar :: ('[FooErr, BarErr] :<< err) => Either (V err) Int

into

foobar :: (LiftVariant '[FooErr, BarErr] err) => Either (V err) Int

[fonghou]

Yes, it type-checks on 2.2 (I was on 2.0.3). Looking at full contraints, it appears that LiftVariant and liftVariant does enforce IsSublist semantics (not IsSubset), Whereas (:<<) and liftVariant' seems enforce weaker IsSubset because of IsMember' ... ~ 'True constraints.

x :: V '[Int,String]
x = V @Int 1

y :: V '[String,Int]
y = liftVariant x

y2 :: (LiftVariant '[Int,String] v) => V v
y2 = liftVariant x
-- y2 @'[Int,String] --> V @Int 1
-- y2 @'[String,Int] --> V @Int 1
-- λ> :t y2
-- y2
--   :: (KnownNat (Haskus.Utils.Types.List.IndexOf' [Char] v v),
--       KnownNat (Haskus.Utils.Types.List.IndexOf' Int v v),
--       Haskus.Utils.Types.List.IsSubset '[Int, String] v ~ 'True) =>
--      V v

y3 :: ([String,Int] :<< v) => V v
y3 = liftVariant' x
-- y3 @'[String,Int] --> V @Int 1
-- y3 @'[Int,String] --> V @Int 1
-- λ> :t y3
-- y3
--   :: (KnownNat (Haskus.Utils.Types.List.IndexOf' Int v v),
--       KnownNat (Haskus.Utils.Types.List.IndexOf' [Char] v v),
--       PopVariant [Char] v, PopVariant Int v,
--       Haskus.Utils.Types.List.IsMember' v [Char] v ~ 'True,
--       Haskus.Utils.Types.List.IsMember' v Int v ~ 'True,
--       Haskus.Utils.Types.List.Index
--         (Haskus.Utils.Types.List.IndexOf' Int v v) v
--       ~ Int,
--       Haskus.Utils.Types.List.Index
--         (Haskus.Utils.Types.List.IndexOf' [Char] v v) v
--       ~ [Char]) =>
--      V v

[hsyl20]

I see. '[String,Int] :<< v provides the necessary witnesses to call liftVariant' (on a Variant whose type is known) but not liftVariant because the latter requires the additional IsSubset constraint. This constraint is supposed to be used to display nicer error messages but they appear randomly (depending on constraint solving order, etc.). I've dropped it on master.

LiftVariant xs ys now implies xs :<< ys. So we get:

y4 :: (LiftVariant' u v) => V u -> V v
y4 = liftVariant'

y5 :: (LiftVariant u v) => V u -> V v
y5 = liftVariant'

> y4 x :: V '[Float]

<interactive>:2:1: error:
    • No instance for (GHC.TypeNats.KnownNat
                         (1
                          GHC.TypeNats.+ Haskus.Utils.Types.List.IndexOf'
                                           [Char] '[] '[Float]))
        arising from a use of ‘y4’
    • In the expression: y4 x :: V '[Float]
      In an equation for ‘it’: it = y4 x :: V '[Float]

> y5 x :: V '[Float]

<interactive>:4:1: error:
    • `Int' is not a member of '[Float]
    • In the expression: y5 x :: V '[Float]
      In an equation for ‘it’: it = y5 x :: V '[Float]

<interactive>:4:1: error:
    • `[Char]' is not a member of '[Float]
    • In the expression: y5 x :: V '[Float]
      In an equation for ‘it’: it = y5 x :: V '[Float]

[fonghou]

Super cool!

Just tried master. liftVariant works perfectly with (:<<) constraint. Thanks again for the awesome library!

[hsyl20]

I have released a new version of the packages that integrate the changes.

@FongHou I've also updated my blog post and the documentation regarding mixing Either and Variant:

• http://hsyl20.fr/home/posts/2018-11-04-trouble-with-typed-errors.html
• https://docs.haskus.org/variant/do_notation.html (should be updated soon)