ยง Contradiction from non-positive occurence

We wish to show that allow non-positive occurences of the inductive type in its constructor can lead to contradiction. Proof as haskell file below: 
{-# LANGUAGE GADTs #-}

data Void where

data F where
  FnSpace :: (F -> Void) -> F

contra :: F -> Void
contra f@(FnSpace fn) = fn f


inhab :: F
inhab = FnSpace contra