content: {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE DeriveGeneric #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE StandaloneDeriving #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE CPP #-}
  {-# LANGUAGE ConstraintKinds #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE DeriveGeneric #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE FunctionalDependencies #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE GeneralizedNewtypeDeriving #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE UndecidableInstances #-}
  {-# OPTIONS_GHC -fno-warn-orphans #-}
  
  -- TODO: I put this in because the below creates a
  --       junk symbol in the measure for headerEth
  {-@ LIQUID "--prune-unsorted" @-}
  
  module ProxyClass where
  
  import           Data.Proxy
  import           GHC.TypeLits (Nat)
  
  type ReadPtrN t  = ReadPtr (t 'Nothing)
  newtype ReadPtr a = ReadPtr Int
  data EthernetHeaderBase m = EHB (m ?$ Bytes 6)
  data ForeignPtr a
  newtype Bytes (n :: Nat) = Bytes (ReadPtr Int)
  
  {-@ foo ::  ReadPtrN EthernetHeaderBase @-}
  foo ::  ReadPtrN EthernetHeaderBase
  foo = undefined
  
  {-@ data EthernetPacket = EthernetPacket
        { headerEth :: ReadPtrN EthernetHeaderBase }
    @-}
  
  data EthernetPacket = EthernetPacket
    { headerEth     :: ReadPtrN EthernetHeaderBase }
  
  infixr 1 ?$
  
  type family (?$) (m :: Maybe (* -> *)) (x :: *) :: * where
    'Just f ?$ x = f x
    'Nothing ?$ x = x
  