Logical contradiction type definitions
Alright, this is the first time I've used Typeclasses so someone feel free to slap me with a tuna if I mess something up.
First of all, I don't understand why the use of &quot;FlexibleInstances&quot; is necessary, and it scares me because these kinds of warnings are usually put in place for a reason. With that out of the way, I'll go through the code.

The first thing you should realize is that in Haskell, typeclasses are basically the same thing as Java's interfaces. They define a contract of behaviour which instances of the class must obey. In this case, the typeclass I'm calling Prop promises the user three methods:

valid to check if the proposition is logically valid (true for all possible inputs)
contradiction to check if the proposition is false for all possible inputs.
lequiv to check if two propositions of the same number of arguments have an identical truth value given the same inputs.

These correspond to three questions which we could ask of any proposition which is a function of any number of propositional atoms. In case you're unfamiliar with this terminology, an 'atom' is one of the inputs to a proposition which is a function taking some number of atoms and itself evaluating to either True or False.
Typeclass Declaration
The name TF for the type class bears no meaning for me, so I changed it to Prop short for &quot;Proposition&quot;.
-- A typeclass which different types may implement.
class Prop p where
  valid         :: p -&gt; Bool            -- Same thing as a Tautism
  contradiction :: p -&gt; Bool            -- False under all conditions/opposite of Tautism
  lequiv        :: p -&gt; p -&gt; Bool   

What we're doing here is creating a new typeclass called Prop. We need the syntax Prop p because we need to define the behaviour of an instance p of the Prop class. If we don't introduce a symbol for it, then how will the compiler know what we're talking about the in the typeclass definition? For example, the line valid :: p -&gt; Bool says that for every instance p of typeclass Prop, there must be a method called valid which maps p to a boolean value. Likewise, there must be a similar method for contradiction.
Now the line lequiv :: p -&gt; p -&gt; Bool may cause some confusion because p appears twice. It's important to understand that p, being an instance of a typeclass, is a type. There are no &quot;objects&quot; as in object-oriented languages. Remember: p is a type which satisfies the typeclass contract given by Prop. The Java equivalent would be a class p implementing an interface Prop. What we're saying here is that for type which implements/is a part of this typeclass Prop, there is a method called lequiv of comparing them. And its type is p -&gt; p -&gt; Bool meaning that it takes in two expressions of type p and returns a boolean indicating whether or not they're equivalent.

Boolean Instance Definition
All we've told the compiler so far are our promises: there will be methods for checking whether an instance of Prop is valid or a contradiction, and a method for comparing two propositions of the same type for equality.
To start, we implement these procedures for the most basic type of proposition: one that is just True or False.
-- This is a proposition which is simply a literal Bool!
instance Prop Bool where
  valid         = id
  contradiction = not
  lequiv b1 b2  = b1 == b2

Here, Prop Bool says that in the expression Prop p above, the type whose behaviour/implementation we're defining is the Bool type. How do we check if a Bool is valid? Well, it takes no arguments, so a proposition that is just True or False is valid if it's true, and otherwise a contradiction.

valid = id says that the function valid mapping our proposition type of Bool to whether or not it's a valid formula is the function id. (This function just returns whatever it's given).
contradiction = not says that the function contradiction mapping the proposition type Bool to whether or not it's a contradiction is the function not. Just as well, because not takes just one Bool as an argument, and returns a Bool. This is compatible with the contract we laid out earlier in the typeclass definition of Prop.
lequiv b1 b2 = (b1 == b2) says that the way of comparing two of these propositions (once again, of type Bool here) for logical equivalence is to simply invoke the already existing method ==.


Inductive Instance Definition - First Step
This is the fun part. We're using induction. Here's the full code snippet, and then I'll break down each line.
instance (Prop p) =&gt; Prop (Bool -&gt; p) where
  valid f         = (valid (f True)) &amp;&amp; (valid (f False))
  lequiv f g      = (lequiv (f True) (g True)) &amp;&amp; (lequiv (f False) (g False))
  contradiction f = (contradiction $ f True) &amp;&amp; (contradiction $ f False)

Now the first line says this: (Bool -&gt; p) is of type Prop, as long as the constraints in what we call the context are met. Here the context is what comes before the =&gt;, and what it says is that p, the type, is a member of the Prop typeclass. This means that we're saying that any type which maps a Bool to any type of Prop is itself an instance of Prop. Why are we doing this? Well, let's start with the simplest case.
Bool is an instance of typeclass Prop, because we defined this 'base case' explicitly. Okay, so then (Bool -&gt; Bool) is also of typeclass prop, because we said that any type (Bool -&gt; &lt;something in class Prop&gt;) is in class Prop. This gives us the functions which take in one boolean argument and return a boolean. Examples: not, id, (\a -&gt; True), (\a -&gt; False). (In fact, these are all such functions).
How have we defined whether to determine whether one of these functions is valid? Our definition says that
valid f = (valid (f True)) &amp;&amp; (valid (f False))

It says that a boolean function f of one boolean is valid if and only if (f True) and (f False) are both valid. Of course, the validity of boolean is just that boolean. So in this case, valid can be thought of as being a bit simpler:
valid f = (f True) &amp;&amp; (f False)

Alright, so f is valid if and only if it evaluates to True for both arguments! That's what we want.
Now for contradiction:
contradiction f = (contradiction $ f True) &amp;&amp; (contradiction $ f False)

This is the key: contradiction asks the question &quot;Is this proposition false for all possible inputs&quot;? To test this, we split f into two parts: its first argument and the rest. If the first argument is True, then is it possible to satisfy proposition f with the remaining arguments? If not, then it's a contradiction. This is the part contradiction $ f True.
f True is itself a function of 1 Bool argument, so it is in class Prop, and so we're able to apply contradiction to it to see if it's a contradiction. We also need to be sure that it's not possible to satisfy f if the first argument is False either, which is why we &amp;&amp; this with contradiction $ f False.
I'll leave the lequiv function as an exercise, and move on to the next inductive step.
Inductive Instance Definition - Inception
Since (Bool -&gt; Bool) is of class Prop, then so too is Bool -&gt; (Bool -&gt; Bool). I could be mistake, but I'm fairly sure that Bool -&gt; Bool -&gt; Bool is actually just short-hand for this. So this means that a boolean function of two boolean variables is itself a proposition. How do we determine its validity? We check if both f True and f False are valid. The former means 'if f True False and f True True both evaluate to True'.
Hopefully you can see now the recursion that's going on (I haven't done a great job explaining it; sorry)-- what we're doing is recursively defining the validity of the type Bool -&gt; Bool -&gt; .... -&gt; Bool so that such a function is valid if and only if it evaluates to True for all possible inputs.