Type Level Check

Question

Let's say I would like to build subtypes that satisfy certain invariants without the help of external tools like LiquidHaskell (ideally I want to do this even without types). What is the most elegant way to do this? So far I have 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 do not export the "Name" constructor from the module, I will have a working solution, because the only way to build an element of this type is through makeValidated.

However, the 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 to fix it?

Answer 1

Underlying is a type function that may not be injective. I.e:

 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 is impossible to say.

It is impossible to call validate unambiguously. To avoid this, the possible correction is to add the "proxy" parameter to your check 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! 

Answer 2

The validate function, as written, is not used in the current GHC. Looking at his signature type:

 validate :: Validated a => Underlying a -> Bool 

you might reasonably think that given the value of type Underlying a , you can figure out which instance of Validated use, namely, a . But this is a mistake: since Underlying not injective, there may be types b and c for which Underlying b ~ Underlying c ; therefore, neither b nor c can be the canonical choice for which instance to use. That is, there is no good mapping of F for types for which F (Underlying a) ~ a always true!

An alternative would be to use a data family rather than a type family.

 class Validated a where data Underlying a validate :: Underlying a -> Bool instance Validated Name where data Underlying Name = Underlying String validate (Underlying name) = ...