Directing type inference with equality constraints and multi parameter type classes

directingTI.hs

{-# LANGUAGE MultiParamTypeClasses 
           , FlexibleInstances
           , TypeFamilies
           #-}

class Add a b where
  add :: a -> b -> a

instance Num a => Add a a where
  add = (+)

{--
two = add (1::Int) 1
-- two would give an error:
--    No instance for (Add Int t)
--      arising from a use of `add' at coercions.hs:12:6-19
--}

{--
nonsense = add (1::Int) 'c'
--    No instance for (Add Int Char)
--      arising from a use of `add' at coercions.hs:23:11-26
--}

class Add' a b where
  add' :: a -> b -> a
  
instance (Num a, a ~ b) => Add' a b where
  add' = (+)
  
two' = add' (1::Int) 1
{--
nonsense' = add' (1::Int) '1'
-- nonsense' would give an error: 
--    Couldn't match expected type `Char' against inferred type `Int'
--    When generalising the type(s) for `nonsense'
--}

main = return ()