Validation at type level

Question

Say I would like to construct subtypes satisfying certain invariants without help of external tools such as LiquidHaskell (ideally I want to do this even without typeclasses). What is the most elegant way to do it? So far I tried the following:

class Validated a where
  type Underlying a
  validate :: Underlying a -> Bool
  construct :: Underlying a -> a
  use :: a -> Underlying a

makeValidated :: Validated a => Underlying a -> Maybe a
makeValidated u = if validate u 
                    then Just (construct u)
                    else Nothing


newtype Name = Name String
instance Validated Name where
  type Underlying Name = String
  validate str = and  [ isUppercase (str !! 0 )
                      , all isLetter str ]
  construct = Name
  use (Name str) = str

I assume that if I don't export the "Name" constructor from the module, I will have a working solution, because the only way to construct an element of the type would be through makeValidated function.

However compiler complains as such:

Could not deduce (Underlying a0 ~ Underlying a)
from the context (Validated a)
  bound by the type signature for
             makeValidated :: Validated a => Underlying a -> Maybe a
  at validated.hs:11:18-55
NB: `Underlying' is a type function, and may not be injective
The type variable `a0' is ambiguous
Possible fix: add a type signature that fixes these type variable(s)
In the first argument of `validate', namely `u'
In the expression: validate u
In the expression:
  if validate u then Just (construct u) else Nothing

How do I fix it?

Answer 1

Underlying is a type function, which might not be injective. That is:

instance Validate T1 where
   type Underlying T1 = Int
   validate = ... -- code A

instance Validate T2 where
   type Underlying T2 = Int
   validate = ... -- code B

Consider now

validate (42 :: Int)

What should this do? Should it call code A or B? Since Underlying T1 = Underlying T2 = Int, it's impossible to tell.

It is impossible to call validate unambiguously. To avoid this, a possible fix is to add a "proxy" parameter to your validation function:

data Proxy a = Proxy

class Validate a where
    validate :: Proxy a -> Underlying a -> Bool

Now you can use:

validate Proxy (42 :: Int)               -- still ambiguous!
validate (Proxy :: Proxy T1) (42 :: Int) -- Now OK!
validate (Proxy :: Proxy T2) (42 :: Int) -- Now OK!