content: {-# LANGUAGE Haskell2010 #-}
  {-# LANGUAGE TypeFamilies, FlexibleContexts #-}
  
  module Class4 where
  
  class  (Eq (Depend s)) => Bug s where
    type Depend s 
    trans :: Depend s -> Depend s
    
  instance Bug Int where
    type Depend Int = ()
    trans = (+1)
  
  check :: (Bug s) => Depend s -> Bool
  check d = d == trans d
  
  {-
   Given: (Bug s, Eq (Depend s))
        = (Bug s, Eq fsk, Depend s ~ fsk)
  
   Wanted: (Eq alpha,                 (invocation of == at alpha)
            Depend s ~ alpha          (first arg of ==)
            Depend sigma ~ alpha      (second arg of ==)
            Bug sigma,                (invocation of trans at sigma)
            Depend sigma ~ Depend s   (first arg of trans)
  
            {der}Eq (Depend sigma)    (superclass of Bug sigma)
  
  ==>
   Wanted: (Eq alpha,                 (invocation of == at alpha)
            Depend s ~ alpha          (first arg of ==)
            Depend sigma ~ alpha      (second arg of ==)
            Bug sigma,                (invocation of trans at sigma)
            {der}Eq (Depend sigma)    (superclass of Bug sigma)
  
  ==>
   Wanted: (Eq alpha,                 (invocation of == at alpha)
            Depend s ~ alpha          (first arg of ==)
            Depend sigma ~ alpha      (second arg of ==)
            Bug sigma,                (invocation of trans at sigma)
  
            {der}Eq uf_ahj
            Depend sigma ~ uf_ahj
  
  ==> uf := alpha
   Wanted: (Eq alpha,                 (invocation of == at alpha)
            Depend s ~ alpha          (first arg of ==)
            Depend sigma ~ alpha      (second arg of ==)
            Bug sigma,                (invocation of trans at sigma)
            {der}Eq alpha)
  ==> discharge Eq alpha from {der}
   Wanted: (Depend s ~ alpha          (first arg of ==)
            Depend sigma ~ alpha      (second arg of ==)
            Bug sigma,                (invocation of trans at sigma)
            {der}Eq alpha)
  
  ==> use given Depend s ~ fsk
   Wanted: (alpha ~ fsk
            Depend sigma ~ alpha      (second arg of ==)
            Bug sigma,                (invocation of trans at sigma)
            {der}Eq alpha)
  
  ==> alpha := fsk
   Wanted: ({given}alpha ~ fsk
            Depend sigma ~ alpha      (second arg of ==)
            Bug sigma,                (invocation of trans at sigma)
            {der}Eq fsk)
  
  ==> discharge {der} Eq fsk
   Wanted: ({given}uf ~ fsk
            Depend sigma ~ uf      (second arg of ==)
            Bug sigma,                (invocation of trans at sigma)
  
  -}
  