blob: 86ab824a1a3a01c6fdf01b23c5ee2d145f8c692a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Coerce (coerce)
import Data.Kind (Type)
import GHC.TypeNats (Nat, type (<=))
f :: (1 <= w)
=> IO (SymBV' sym w)
-> IO (SymBV sym w)
f = coerce
----
data BaseType = BaseBVType Nat
type family SymExpr (sym :: Type) :: BaseType -> Type
type SymBV sym n = SymExpr sym (BaseBVType n)
newtype SymBV' sym w = MkSymBV' (SymBV sym w)
|
