How to prove double negation for type level booleans?

Question

I have the following module:

{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, RoleAnnotations #-}
module Main where

import Data.Coerce (coerce)

-- logical negation for type level booleans
type family Not (x :: Bool) where
    Not True = False
    Not False = True

-- a 3D vector with a phantom parameter that determines whether this is a
-- column or row vector
data Vector (isCol :: Bool) = Vector Double Double Double

type role Vector phantom

-- convert column to row vector or row to column vector
flipVec :: Vector isCol -> Vector (Not isCol)
flipVec = coerce

-- scalar product is only defined for vectors of different types
-- (row times column or column times row vector)
sprod :: Vector isCol -> Vector (Not isCol) -> Double
sprod (Vector x1 y1 z1) (Vector x2 y2 z2) = x1*x2 + y1*y2 + z1*z2

-- vector norm defined in terms of sprod
norm :: Vector isCol -> Double
-- this definition compiles
norm v = sqrt (v `sprod` flipVec v)
-- this does not (without an additional constraint, see below)
norm v = sqrt (flipVec v `sprod` v)

main = undefined

The second definition of norm does not compile, because flipVec v returns Vector (Not isCol) and hence sprod wants a Vector (Not (Not isCol)) as second argument:

Main.hs:22:34:                                                                                                                      
    Couldn't match type ‘isCol’ with ‘Not (Not isCol)’                                                                              
      ‘isCol’ is a rigid type variable bound by                                                                                     
              the type signature for norm :: Vector isCol -> Double                                                                 
              at Main.hs:20:9                                                                                                       
    Expected type: Vector (Not (Not isCol))                                                                                         
      Actual type: Vector isCol                                                                                                     
    Relevant bindings include                                                                                                       
      v :: Vector isCol (bound at Main.hs:22:6)                                                                                     
      norm :: Vector isCol -> Double (bound at Main.hs:22:1)                                                                        
    In the second argument of ‘sprod’, namely ‘v’                                                                                   
    In the first argument of ‘sqrt’, namely ‘(flipVec v `sprod` v)’

I could of course add the constraint isCol ~ Not (Not isCol) to the type of norm:

norm :: isCol ~ Not (Not isCol) => Vector isCol -> Double

At the call site, the actual value of isCol is known and the compiler will see that this constraint is indeed satisfied. But it seems weird that the implementation details of norm are leaking into the type signature.

My question: is it possible to somehow convince the compiler that isCol ~ Not (Not isCol) is always true, so that the superfluous constraint is not necessary?

Answer 1

The answer: yes, it is. The proof is quite trivial if you have the correct datatypes:

data family Sing (x :: k) 

class SingI (x :: k) where 
  sing :: Sing x 

data instance Sing (x :: Bool) where 
  STrue :: Sing True 
  SFalse :: Sing False 

type SBool x = Sing (x :: Bool)

data (:~:) x y where 
  Refl :: x :~: x 

double_neg :: SBool x -> x :~: Not (Not x) 
double_neg x = case x of 
                 STrue -> Refl 
                 SFalse -> Refl 

As you can see, the compiler will see that the proof is trivial upon inspection of the different cases. You'll find all of these data definitions in several packages, for example singletons. You use the proof like so:

instance Sing True where sing = STrue 
instance Sing False where sing = SFalse

norm :: forall isCol . SingI isCol => Vector isCol -> Double
norm v = case double_neg (sing :: Sing isCol) of 
           Refl -> sqrt (flipVec v `sprod` v)

Of course this a lot of work for such a trivial thing. If you are really sure you know what you're doing, you can "cheat":

import Unsafe.Coerce
import Data.Proxy 

double_neg' :: Proxy x -> x :~: Not (Not x) 
double_neg' _ = unsafeCoerce (Refl :: () :~: ())

This allows you to get rid of the SingI constraint:

norm' :: forall isCol . Vector isCol -> Double
norm' v = case double_neg' (Proxy :: Proxy isCol) of 
           Refl -> sqrt (flipVec v `sprod` v)