This is a variation on an old chestnut. I wrote it expecting it not to work, but it did. Or is it dodgy? (At GHC 8.6.5.)
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts,
FunctionalDependencies, UndecidableInstances, GADTs,
PatternSignatures #-} -- deprecated, but we're not using ScopedTypeVariables
-- 3-way FunDep for Nats Add ??
data ZNat = ZNat deriving (Eq, Show, Read)
data SNat a = SNat a deriving (Eq, Show, Read)
oneNat = SNat ZNat
twoNat = SNat oneNat
class AddNat a b c | a b -> c, a c -> b, b c -> a where -- full 3 FunDeps
addNat :: a -> b -> c
instance AddNat ZNat b b where
addNat _ y = y
instance {-# OVERLAPPABLE #-} (a ~ SNat a', c ~ SNat c', AddNat a' b c')
=> AddNat a b c where
addNat (SNat x) y = SNat (addNat x y)
subNat (_ :: c) (_ :: b) = reflNat :: (AddNat a b c, ReflNat a) => a
-- test:
-- *Main> :t subNat twoNat oneNat
-- subNat twoNat oneNat :: SNat ZNat
class ReflNat a where reflNat :: a -- for ref
instance ReflNat ZNat where reflNat = ZNat
instance (ReflNat a') => ReflNat (SNat a') where
reflNat = (SNat (reflNat :: ReflNat aa => aa))
Traditionally there's only two FunDeps on class AddNat, and that second instance is
instance ( AddNat a' b c')
=> AddNat (SNat a') b (SNat c') where
addNat (SNat x) y = SNat (addNat x y) -- implementation is the same
That instance would get rejected Functional dependencies conflict between instance declarations: if there were FunDep b c -> a. As it is, the OVERLAPPABLE instance is exploiting GHC's bogus FunDep consistency check.
But without that FunDep, subNat can't infer its result from the arguments: Ambiguous type variable 'a0'. I'm guessing my test works because the types of the arguments to subNat are known in full. If they were partially known, type improvement would get stuck unable to reject the ZNat b b instance.
Oleg Kiselyov's ftp site used to have a class for 3-way improvement of adding naturals, but that had a complex rat's nest of auxiliary superclass constraints and auxiliary instances that essentially repeated the central class. What I've done seems too simplistic. Where will it go wrong?