copilot-core: Add Show instance for Type. Refs #589.

Currently, the `Copilot.Theorem.What4.prove` function returns a list of
results, where each result contains a `SatResult` that describes whether a
property is `Valid`, `Invalid`, or `Unknown`. The `Invalid` result has the
limitation that it does not give any information about a specific
counterexample that could drive Copilot into falsifying the property, however.
This makes it challenging to interpret what the results of prove mean.

To define a companion function to `prove` that also returns counterexample
information upon a failed proof, it is convenient to be able to display `Type`
information in panic messages.

This commit derives a basic `Show` instance for `Type` so that
`copilot-theorem` can display them whenever an internal invariant is violated.

Author: RyanGlScott

copilot-core/src/Copilot/Core/Type.hs

@@ -5,6 +5,7 @@
 {-# LANGUAGE GADTs                     #-}
 {-# LANGUAGE KindSignatures            #-}
 {-# LANGUAGE ScopedTypeVariables       #-}
+{-# LANGUAGE StandaloneDeriving        #-}
 {-# LANGUAGE Trustworthy               #-}
 {-# LANGUAGE TypeApplications          #-}
 {-# LANGUAGE TypeOperators             #-}
@@ -154,6 +155,7 @@ data Type :: * -> * where
                          , Typed t
                          ) => Type t -> Type (Array n t)
   Struct :: (Typed a, Struct a) => a -> Type a
+deriving instance Show (Type a)
 
 -- | Return the length of an array from its type
 typeLength :: forall n t . KnownNat n => Type (Array n t) -> Int