blob: 68d681c19f3c163919bfc8a27d77784a99188d75 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
{-# LANGUAGE DataKinds, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-}
{-# OPTIONS_GHC -O0 -freduction-depth=500 #-}
module T13386 where
import GHC.TypeLits
type DivisibleBy x y = Help x y 0 (CmpNat x 0)
type family Help x y z b where
Help x y z EQ = True
Help x y z LT = False
Help x y z GT = Help x y (z+y) (CmpNat x z)
foo :: DivisibleBy y 3 ~ True => proxy y -> ()
foo _ = ()
type N = 1002
k = foo @N undefined
|
