Add Hunk invariant static checks

[ninioArtillero]

This PR introduces Liquid Haskell static checks for the ContextSize to be a natural number and for the documented type Hunk c = [Diff [c]] invariant:

-- No two consecutive elements in a 'Hunk' are both applications
-- of 'First', 'Second', or 'Both', i.e. the list does not stutter
-- on 'Diff' constructors.

Without introducing any semantic change.

The Hunk invariant is encoded using a refinement type alias of the same name with a noStuttering predicate. Most notably, this is non-trivially checked in getContextDiffNumbered postcondition by specifying its local functions doPrefix and doSuffix to transform an input Hunk into an intermediate form {ds : [ValidListDiff c c] | noFFSS ds} that splitBothBoth transforms back into a Hunk. The input Hunk (actually a stronger variant which also specifies the value contents to be non-empty) is produced by getGroupedDiffBy.

The changes within getGroupedDiffBy are just reformating (to better accomodate the Liquid Haskell specifications) and the following renamings to improve readability:

go -> groupDiff
goFirsts -> leadingFirstss
goSeconds -> leading Seconds
goBoth -> leadingBoths

NOTE: Refinement type aliases--such as {-@ type Hunk c = { h : [ValidListDiff c c] | noStuttering h} @-} and {-@ type ContextDiff c = [Hunk c] @-}--override the corresponding type aliases--type Hunk c = [Diff [c]] and type Hunk c = [Diff [c] respectively--in Liquid Haskell specifications.

PolyDiff and Diff types and instances are moved to a new Data.Algorithm.Diff.Type module. This move is required to have functions defined solely for Liquid Haskell specifications in a separate module and avoid cyclic dependency; this helps prevent the cluther of implementation modules by (some of the) unused functions. Such functions reside in Data.Algorithm.Diff.Refinement, together with refinement type aliases that use them and other helpers required for specifications.