blob: ce86d7beabe49b742b66a667db1a1557cfc409ae (
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
26
27
28
29
30
31
|
{-# LANGUAGE TypeFamilies, FlexibleContexts, EmptyDataDecls #-}
module SkolemOccursLoop where
-- SkelemOccurs tests by Tom and Martin
data T x
type family F x
type instance F [x] = [T (F x)]
t :: a -> a -> Bool
t _ _ = True
f :: a -> F [a]
f = undefined
test1 :: (F [a] ~ a) => a -> Bool
test1 x = t x (f x)
--
data S a
type family G x
type instance G (S x, y) = S (G (x,y))
g :: a -> G [a]
g = undefined
test2 :: (G (S a,a) ~ a) => a -> Bool
-- inferred: G [a] ~ a => a -> Bool
test2 x = t x (g x)
|
