changes for ghc-9

[jwaldmann]

not all for ghc-9, some are required earlier.

 import Data.GADT.Show
+import Data.Type.Equality ((:~:)(Refl))
 import Data.GADT.Compare

and import package some, because of
https://github.com/obsidiansystems/dependent-sum/blob/73ab6cb23331f463c384290b4a1be542e68b323d/dependent-sum/ChangeLog.md#0621---2020-03-21

[jwaldmann]

There were several failable pattern matches, which would require MonadFail , which would later not match runIdentity. So I decided to leave the type constraint at Monad, and introduce a partial function

+unJust m = m >>= \ case Just x -> return x

and change pattern matches as in

-      Just errCond <- compositeGEQ idx (bound arr)
+      errCond <- unJust $ compositeGEQ idx (bound arr)

for the few failable matches at other types, I used LambdaCase directly