Boolean refinements "weak"

[NeQuissimus]

The title sucks, I know :)

The following is an annoying thing refined allows but should probably not be allowed. I also think that some kind of type bound or self-typing may be able to solve this, although I have not looked into it at all.

Imagine this code:

type Foo = String Refined NonEmpty And MaxSize[W.`10`.T]

Looks fine until you realize it makes no sense at all (but compiles!).

typeOf[Foo].dealias.toString 
res23: String = "eu.timepit.refined.boolean.And[eu.timepit.refined.api.Refined[String,eu.timepit.refined.collection.NonEmpty],eu.timepit.refined.collection.MaxSize[Int(10)]]"

So we have an And[Refined[String, NonEmpty], MaxSize[10]]. Is there an actual use case for Refined being a type parameter to any of the boolean operators? I can't think of one.

What I actually would want is this:

type Foo = String Refined (NonEmpty And MaxSize[W.`10`.T])
 typeOf[Foo].dealias.toString 
res21: String = "eu.timepit.refined.api.Refined[String,eu.timepit.refined.boolean.And[eu.timepit.refined.collection.NonEmpty,eu.timepit.refined.collection.MaxSize[Int(10)]]]"

To my understanding, there is no way we can make Refined "weaker". But this should at least be a compile error without the parentheses, should it not?

[fthomas]

We could introduce a marker trait Predicate, let every predicate extends that, and then use a type bound in And: class And[A <: Predicate, B <: Predicate]. Refined would not be a Predicate and And[Refined, ...] would be a compile error.

[NeQuissimus]

I like that, I will likely send a PR for it next week.

[fthomas]

That would be great!

[NeQuissimus]

Here is another weird one. I am unsure it will be fixed with the marker trait. If not, I will open a new issue:

type Foo = String Refined MaxSize[W.`10`.T] //compiles, makes no sense
type Bar = String Refined MaxSize[Equal[W.`10`.T]] // what you actually want

[fthomas]

Actually the first is correct and the second makes no sense. But you're right, for MaxSize we can't add a type bound because we want to allow both Nat and singleton types: MaxSize[_5] and MaxSize[W.`5`.T].

What we can prevent via the marker trait is:

type Foo = String Refined Size[W.`10`.T] //compiles, makes no sense
type Bar = String Refined Size[Equal[W.`10`.T]] // what you actually want

By defining Size as final case class Size[P <: Predicate](p: P).

[NeQuissimus]

So this marker trait business is a little more involved than I had thought :) If somebody want to take this on, go ahead. Otherwise it will have to wait until I have a bit more free time.

[fthomas]

Oh, I see the issue. We also put Result values in e.g. Not(Result(...)) and other predicates in Validate instances and Result is not a predicate. Hmm...

[fthomas]

We are not only putting Result values into predicates but sometimes also arbitrary types. See for example

scala> Validate[List[Int], Forall[Positive]].validate(List(1, 2))
res1: Result[Forall[List[Result[Greater[shapeless._0]]]]] = Passed(Forall(List(Passed(Greater(shapeless._0@5d15faf4)), Passed(Greater(shapeless._0@5d15faf4)))))

So if we change class Forall[P](p: P) to class Forall[P <: Predicate](p: P) the above would be invalid since List is not a subtype of Predicate.

[NeQuissimus]

Yeah, I don't think we can do this with what we currently have. I have sort of given up since I've run into lots of different issues whenever I tried... Not sure how to solve this...