Simon Peyton Jones pushed to branch wip/T26315 at Glasgow Haskell Compiler / GHC
Commits:
-
643d10bc
by Simon Peyton Jones at 2025-09-10T08:46:08+01:00
2 changed files:
Changes:
| 1 | +{-# LANGUAGE DataKinds #-}
|
|
| 2 | +{-# LANGUAGE GADTs #-}
|
|
| 3 | +{-# LANGUAGE QuantifiedConstraints #-}
|
|
| 4 | +{-# LANGUAGE UndecidableInstances #-}
|
|
| 5 | + |
|
| 6 | +module T26396 where
|
|
| 7 | + |
|
| 8 | +import Data.Kind
|
|
| 9 | +import Data.Type.Equality
|
|
| 10 | +import GHC.TypeNats
|
|
| 11 | + |
|
| 12 | +newtype Vector (el :: Type) (len :: Natural) = Vector [el]
|
|
| 13 | + deriving (Eq)
|
|
| 14 | + |
|
| 15 | +data Sized (f :: Natural -> Type) where
|
|
| 16 | + Sized :: KnownNat len => f len -> Sized f
|
|
| 17 | + |
|
| 18 | +instance (forall (len :: Natural). Eq (f len)) => Eq (Sized f) where
|
|
| 19 | + Sized xs == Sized ys = case sameNat xs ys of
|
|
| 20 | + Nothing -> False
|
|
| 21 | + Just Refl -> xs == ys
|
|
| 22 | + |
|
| 23 | +newtype Foo (el :: Type) = Foo (Sized (Vector el))
|
|
| 24 | + deriving (Eq) |
| ... | ... | @@ -154,3 +154,4 @@ test('T24955b', normal, compile, ['']) |
| 154 | 154 | test('T24955c', normal, compile, [''])
|
| 155 | 155 | test('T25148c', normal, compile, [''])
|
| 156 | 156 | test('deriving-inferred-ty-arg', normal, compile, ['-ddump-deriv -dsuppress-uniques'])
|
| 157 | +test('T26396', normal, compile, ['']) |