Disable Haskell type coercion

I have example based on hyperloglog. I'm trying to parametrize my Container with size, and use reflection to use this parameter in functions on containers.

import           Data.Proxy
import           Data.Reflection

newtype Container p = Container { runContainer :: [Int] }
    deriving (Eq, Show)

instance Reifies p Integer => Monoid (Container p) where
  mempty = Container $ replicate (fromIntegral (reflect (Proxy :: Proxy p))) 0
  mappend (Container l) (Container r) = undefined

My lame Monoid instance defines mempty based on reified parameter, and doing some "type-safe" mappend. It works perfectly when I'm trying to sum containers of different size, failing with type error.

However it's still can be tricked with coerce, and I'm looking for way to block it at compile time:

ghci> :set -XDataKinds
ghci> :m +Data.Coerce
ghci> let c3 = mempty :: Container 3
ghci> c3
ghci> Container {runContaner: [0,0,0]}
ghci> let c4 = coerce c3 :: Container 4
ghci> :t c4
ghci> c4 :: Container 4
ghci> c4
ghci> Container {runContainer: [0,0,0]}

Adding type role doesn't help

type role Container nominal

Solution

The issue is that newtypes are coercible to their representation as long as the constructor is in scope – indeed, this is a big part of the motivation for Coercible. And Coercible constraints are like any other type class constraint, and are automatically searched and put together for you, only even more so. Thus, coerce c3 is finding that you have

instance Coercible (Container p) [Int]
instance Coercible [Int] (Container p')

for all p and p', and happily building the composite coercion for you via

instance (Coercible a b, Coercible b c) => Coercible a c

If you don't export the Container constructor – as you probably want to do anyway! – then it's no longer known that the newtype is equal to its representation (you lose the first two instances above), and you get the desired error in other modules:

ContainerClient.hs:13:6:
    Couldn't match type ‘4’ with ‘3’
    arising from trying to show that the representations of
      ‘Container 3’ and
      ‘Container 4’ are the same
    Relevant role signatures: type role Container nominal nominal
    In the expression: coerce c3
    In an equation for ‘c4’: c4 = coerce c3

However, you'll always be able to break your invariants in the module where you define the newtype (via coerce or otherwise).

As a side note, you probably don't want to use a record-style accessor here and export it; that lets users use record-update syntax to change out code from under you, so

c3 :: Container 3
c3 = mempty

c3' :: Container 3
c3' = c3{runContainer = []}

becomes valid. Make runContainer a free-standing function instead.

We can verify that we're getting the composition of the two newtype-representation constraints by looking at the Core (via -ddump-simpl): within the module that defines Container (which I've also called Container), the output is (if we remove the export list)

c4 :: Container 4
[GblId, Str=DmdType]
c4 =
  c3
  `cast` (Container.NTCo:Container[0] <GHC.TypeLits.Nat>_N <3>_N
          ; Sym (Container.NTCo:Container[0] <GHC.TypeLits.Nat>_N <4>_N)
          :: Container 3 ~R# Container 4)

It's a bit hard to read, but the important thing to see is Container.NTCo:Container[0]: the NTCo is a newtype coercion between the newtype Container p and its representation type. Sym turns this around, and ; composes two constraints.

Call the final constraint γₓ; then the whole typing derivation is

Sym :: (a ~ b) -> (b ~ a)
-- Sym is built-in

(;) :: (a ~ b) -> (b ~ c) -> (a ~ c)
-- (;) is built-in

γₙ :: k -> (p :: k) -> Container p ~ [Int]
γₙ k p = Container.NTCo:Container[0] <k>_N <p>_N

γ₃ :: Container 3 ~ [Int]
γ₃ = γₙ GHC.TypeLits.Nat 3

γ₄ :: Container 4 ~ [Int]
γ₄ = γₙ GHC.TypeLits.Nat 4

γ₄′ :: [Int] ~ Container 4
γ₄′ = Sym γ₄

γₓ :: Container 3 ~ Container 4
γₓ = γ₃ ; γ₄′

Here are the source files I used:

Container.hs:

{-# LANGUAGE FlexibleContexts, UndecidableInstances, ScopedTypeVariables,
             RoleAnnotations, PolyKinds, DataKinds #-}

module Container (Container(), runContainer) where

import Data.Proxy
import Data.Reflection
import Data.Coerce

newtype Container p = Container { runContainer :: [Int] }
    deriving (Eq, Show)
type role Container nominal

instance Reifies p Integer => Monoid (Container p) where
  mempty = Container $ replicate (fromIntegral (reflect (Proxy :: Proxy p))) 0
  mappend (Container l) (Container r) = Container $ l ++ r

c3 :: Container 3
c3 = mempty

-- Works
c4 :: Container 4
c4 = coerce c3

ContainerClient.hs:

{-# LANGUAGE DataKinds #-}

module ContainerClient where

import Container
import Data.Coerce

c3 :: Container 3
c3 = mempty

-- Doesn't work :-)
c4 :: Container 4
c4 = coerce c3