Skip to content

Instantly share code, notes, and snippets.

@RyanGlScott
Last active May 19, 2021
Embed
What would you like to do?
Is this use of unsafeCoerce valid?
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall #-}
module Main (main) where
import Data.Functor.Identity
import Data.Proxy
import Data.Type.Equality ((:~:)(..))
import GHC.TypeNats
import Numeric.Natural
import qualified Prelude
import Prelude hiding (length)
import Unsafe.Coerce (unsafeCoerce)
main :: IO ()
main = print $
let Just v = fromList (knownNat @2) [knownNat @1, knownNat @1]
in joinWith (\_ w l -> addNat w l) knownNat v
-----
-- parameterized-utils
-----
newtype NatRepr (n::Nat) = NatRepr Natural
instance Show (NatRepr n) where
show (NatRepr n) = show n
knownNat :: forall n . KnownNat n => NatRepr n
knownNat = NatRepr (natVal (Proxy :: Proxy n))
maxInt :: Natural
maxInt = fromIntegral (maxBound :: Int)
widthVal :: NatRepr n -> Int
widthVal (NatRepr i) | i <= maxInt = fromIntegral i
| otherwise = error ("Width is too large: " ++ show i)
addNat :: NatRepr m -> NatRepr n -> NatRepr (m+n)
addNat (NatRepr m) (NatRepr n) = NatRepr (m+n)
data LeqProof (m :: Nat) (n :: Nat) where
LeqProof :: (m <= n) => LeqProof m n
testStrictLeq :: forall m n
. (m <= n)
=> NatRepr m
-> NatRepr n
-> Either (LeqProof (m+1) n) (m :~: n)
testStrictLeq (NatRepr m) (NatRepr n)
| m < n = Left (unsafeCoerce (LeqProof :: LeqProof 0 0))
| otherwise = Right (unsafeCoerce (Refl :: m :~: m))
{-# NOINLINE testStrictLeq #-}
leqRefl :: forall f n . f n -> LeqProof n n
leqRefl _ = LeqProof
leqSub2 :: LeqProof x_l x_h
-> LeqProof y_l y_h
-> LeqProof (x_l-y_h) (x_h-y_l)
leqSub2 LeqProof LeqProof = unsafeCoerce (LeqProof :: LeqProof 0 0)
{-# NOINLINE leqSub2 #-}
leqMulCongr :: LeqProof a x
-> LeqProof b y
-> LeqProof (a*b) (x*y)
leqMulCongr LeqProof LeqProof = unsafeCoerce (LeqProof :: LeqProof 1 1)
{-# NOINLINE leqMulCongr #-}
leqMulPos :: forall p q x y
. (1 <= x, 1 <= y)
=> p x
-> q y
-> LeqProof 1 (x*y)
leqMulPos _ _ = leqMulCongr (LeqProof :: LeqProof 1 x) (LeqProof :: LeqProof 1 y)
lemmaMul :: (1 <= n) => p w -> q n -> (w + (n-1) * w) :~: (n * w)
lemmaMul = unsafeCoerce Refl
{-# NOINLINE lemmaMul #-}
data Vector n a where
Vector :: (1 <= n) => !(VVector a) -> Vector n a
length :: Vector n a -> NatRepr n
length (Vector xs) = NatRepr (fromIntegral (vlength xs) :: Natural)
{-# INLINE length #-}
nonEmpty :: Vector n a -> LeqProof 1 n
nonEmpty (Vector _) = LeqProof
{-# Inline nonEmpty #-}
uncons :: forall n a. Vector n a -> (a, Either (n :~: 1) (Vector (n-1) a))
uncons v@(Vector xs) = (vhead xs, mbTail)
where
mbTail :: Either (n :~: 1) (Vector (n - 1) a)
mbTail = case testStrictLeq (knownNat @1) (length v) of
Left n2_leq_n ->
do LeqProof <- return (leqSub2 n2_leq_n (leqRefl (knownNat @1)))
return (Vector (vtail xs))
Right Refl -> Left Refl
{-# Inline uncons #-}
fromList :: (1 <= n) => NatRepr n -> [a] -> Maybe (Vector n a)
fromList n xs
| widthVal n == vlength v = Just (Vector v)
| otherwise = Nothing
where
v = vfromList xs
{-# INLINE fromList #-}
joinWithM ::
forall m f n w.
(1 <= w, Monad m) =>
(forall l. (1 <= l) => NatRepr l -> f w -> f l -> m (f (w + l)))
-> NatRepr w
-> Vector n (f w)
-> m (f (n * w))
joinWithM jn w = fmap fst . go
where
go :: forall l. Vector l (f w) -> m (f (l * w), NatRepr (l * w))
go exprs =
case uncons exprs of
(a, Left Refl) -> return (a, w)
(a, Right rest) ->
case nonEmpty rest of { LeqProof ->
case leqMulPos (length rest) w of { LeqProof ->
case nonEmpty exprs of { LeqProof ->
case lemmaMul w (length exprs) of { Refl -> do
(res, sz) <- go rest
joined <- jn sz a res
return (joined, addNat w sz)
}}}}
joinWith ::
forall f n w.
(1 <= w) =>
(forall l. (1 <= l) => NatRepr l -> f w -> f l -> f (w + l))
-> NatRepr w
-> Vector n (f w)
-> f (n * w)
joinWith jn w v = runIdentity $ joinWithM (\n x -> pure . (jn n x)) w v
{-# Inline joinWith #-}
-- The real @parameterized-utils@ library uses 'Vector' from the @vector@
-- library. However, that isn't necessary to trigger the bug, so to avoid
-- incurring a dependency on @vector@, we simulate it with a linked list.
type VVector a = [a]
vfromList :: [a] -> VVector a
vfromList = id
vhead :: VVector a -> a
vhead = head
vlength :: VVector a -> Int
vlength = Prelude.length
vtail :: VVector a -> [a]
vtail = tail
############
# With -O0 #
############
$ rm -f *.hi *.o && /opt/ghc/8.6.5/bin/ghc -O0 Main.hs && ./Main
[1 of 1] Compiling Main ( Main.hs, Main.o )
Linking Main ...
Main: internal error: stg_ap_pp_ret
(GHC version 8.6.5 for x86_64_unknown_linux)
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
Aborted (core dumped)
$ rm -f *.hi *.o && /opt/ghc/8.8.4/bin/ghc -O0 Main.hs && ./Main
[1 of 1] Compiling Main ( Main.hs, Main.o )
Linking Main ...
Main: internal error: stg_ap_pp_ret
(GHC version 8.8.4 for x86_64_unknown_linux)
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
Aborted (core dumped)
$ rm -f *.hi *.o && /opt/ghc/8.10.4/bin/ghc -O0 Main.hs && ./Main
[1 of 1] Compiling Main ( Main.hs, Main.o )
Linking Main ...
Main: internal error: stg_ap_pp_ret
(GHC version 8.10.4 for x86_64_unknown_linux)
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
Aborted (core dumped)
$ rm -f *.hi *.o && /opt/ghc/9.0.1/bin/ghc -O0 Main.hs && ./Main
[1 of 1] Compiling Main ( Main.hs, Main.o )
Linking Main ...
Main: internal error: stg_ap_pp_ret
(GHC version 9.0.1 for x86_64_unknown_linux)
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
Aborted (core dumped)
############
# With -O1 #
############
$ rm -f *.hi *.o && /opt/ghc/8.6.5/bin/ghc -O1 Main.hs && ./Main
[1 of 1] Compiling Main ( Main.hs, Main.o )
Linking Main ...
Main: internal error: stg_ap_pp_ret
(GHC version 8.6.5 for x86_64_unknown_linux)
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
Aborted (core dumped)
$ rm -f *.hi *.o && /opt/ghc/8.8.4/bin/ghc -O1 Main.hs && ./Main
[1 of 1] Compiling Main ( Main.hs, Main.o )
Linking Main ...
Main: internal error: stg_ap_pp_ret
(GHC version 8.8.4 for x86_64_unknown_linux)
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
Aborted (core dumped)
$ rm -f *.hi *.o && /opt/ghc/8.10.4/bin/ghc -O1 Main.hs && ./Main
[1 of 1] Compiling Main ( Main.hs, Main.o )
Linking Main ...
Main: internal error: stg_ap_pp_ret
(GHC version 8.10.4 for x86_64_unknown_linux)
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
Aborted (core dumped)
$ rm -f *.hi *.o && /opt/ghc/9.0.1/bin/ghc -O1 Main.hs && ./Main
[1 of 1] Compiling Main ( Main.hs, Main.o )
Linking Main ...
2
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment