blob: 180472232fda66bc7af950fb435abb5317194c16 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
{-# LANGUAGE RankNTypes, TypeFamilies #-}
-- Unification yielding a coercion under a forall
module Data.Vector.Unboxed where
import Control.Monad.ST ( ST )
import Data.Kind (Type)
data MVector s a = MV
data Vector a = V
type family Mutable (v :: Type -> Type) :: Type -> Type -> Type
type instance Mutable Vector = MVector
create :: (forall s. MVector s a) -> Int
create = create1
-- Here we get Couldn't match expected type `forall s. MVector s a'
-- with actual type `forall s. Mutable Vector s a1'
-- Reason: when unifying under a for-all we don't solve type
-- equalities. Think more about this.
create1 :: (forall s. Mutable Vector s a) -> Int
create1 _ = error "urk"
|