blob: 59a7ace8ba560cbe3c3e4c08f42ffe2689a1c3f9 (
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
32
33
34
35
36
37
38
39
40
41
|
{-# OPTIONS_GHC -Wno-redundant-constraints -Wno-simplifiable-class-constraints #-}
{-# LANGUAGE TypeFamilies, EmptyDataDecls, FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
module NonLinearLHS where
type family E a b
type instance E a a = [a]
foo :: E [Int] (E Int Int) -> Int
foo = sum . concat
data family F a b
data instance F a a = MkF [a]
goo :: F Int Int -> F Bool Bool
goo (MkF xs) = MkF $ map odd xs
-- HList-like type equality
data True; data False;
type family EqTy a b
type instance EqTy a a = True
class EqTyP a b result
instance (EqTy a b ~ isEq, Proxy isEq result) => EqTyP a b result
class Proxy inp out
instance (result ~ True) => Proxy True result
instance (result ~ False) => Proxy notTrue result
testTrue :: EqTyP Int Int r => r
-- Weird test case: (EqTyP Int Int) is simplifiable
testTrue = undefined
testFalse :: EqTyP Int Bool r => r
-- Weird test case: (EqTyP Int Bool) is simplifiable
testFalse = undefined
|
