Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: 8016561f by Simon Peyton Jones at 2025-07-08T07:41:13-04:00 Add a test for T26176 - - - - - 454cd682 by Simon Peyton Jones at 2025-07-08T07:41:13-04:00 Add test for #14010 This test started to work in GHC 9.6 and has worked since. This MR just adds a regression test - - - - - 5 changed files: - + testsuite/tests/indexed-types/should_fail/T26176.hs - + testsuite/tests/indexed-types/should_fail/T26176.stderr - testsuite/tests/indexed-types/should_fail/all.T - + testsuite/tests/typecheck/should_compile/T14010.hs - testsuite/tests/typecheck/should_compile/all.T Changes: ===================================== testsuite/tests/indexed-types/should_fail/T26176.hs ===================================== @@ -0,0 +1,32 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeFamilies #-} +module T26176 where + +-- In a previous version of GHC this test led to +-- a very misleading error message + +import GHC.TypeNats + +data T = X +type family FA t where FA X = 1 +type family FB t where FB X = 2 + +foo :: forall p (t :: T). p t +foo = undefined + where + a :: SNat 5 + a = b + + b :: SNat (FA t) + b = undefined + + c :: SNat 3 + c = d + + d :: SNat (FB t) + d = undefined + + x = bar @t + +bar :: FA t <= FB t => p t +bar = undefined ===================================== testsuite/tests/indexed-types/should_fail/T26176.stderr ===================================== @@ -0,0 +1,41 @@ +T26176.hs:18:7: error: [GHC-83865] + • Couldn't match type ‘FA t’ with ‘5’ + Expected: SNat 5 + Actual: SNat (FA t) + • In the expression: b + In an equation for ‘a’: a = b + In an equation for ‘foo’: + foo + = undefined + where + a :: SNat 5 + a = b + b :: SNat (FA t) + b = undefined + .... + • Relevant bindings include + b :: SNat (FA t) (bound at T26176.hs:21:3) + d :: SNat (FB t) (bound at T26176.hs:27:3) + x :: p0 t (bound at T26176.hs:29:3) + foo :: p t (bound at T26176.hs:15:1) + +T26176.hs:24:7: error: [GHC-83865] + • Couldn't match type ‘FB t’ with ‘3’ + Expected: SNat 3 + Actual: SNat (FB t) + • In the expression: d + In an equation for ‘c’: c = d + In an equation for ‘foo’: + foo + = undefined + where + a :: SNat 5 + a = b + b :: SNat (FA t) + b = undefined + .... + • Relevant bindings include + d :: SNat (FB t) (bound at T26176.hs:27:3) + x :: p0 t (bound at T26176.hs:29:3) + foo :: p t (bound at T26176.hs:15:1) + ===================================== testsuite/tests/indexed-types/should_fail/all.T ===================================== @@ -172,3 +172,4 @@ test('T21896', normal, compile_fail, ['']) test('HsBootFam', [extra_files(['HsBootFam_aux.hs','HsBootFam_aux.hs-boot'])], multimod_compile_fail, ['HsBootFam', '']) test('BadFamInstDecl', [extra_files(['BadFamInstDecl_aux.hs'])], multimod_compile_fail, ['BadFamInstDecl', '']) test('T19773', [], multimod_compile_fail, ['T19773', '-Wall']) +test('T26176', normal, compile_fail, ['']) ===================================== testsuite/tests/typecheck/should_compile/T14010.hs ===================================== @@ -0,0 +1,44 @@ +{-# LANGUAGE NoImplicitPrelude, PolyKinds, DataKinds, TypeFamilies, + UndecidableSuperClasses, RankNTypes, TypeOperators, + FlexibleContexts, TypeSynonymInstances, FlexibleInstances, + UndecidableInstances #-} +module Monolith where + +import Data.Kind (Type) +import GHC.Exts (Constraint) + +type family (~>) :: c -> c -> Type + +type instance (~>) = (->) +type instance (~>) = ArrPair + +type family Fst (p :: (a, b)) :: a where + Fst '(x, _) = x + +type family Snd (p :: (a, b)) :: b where + Snd '(_, y) = y + +data ArrPair a b = ArrPair (Fst a ~> Fst b) (Snd a ~> Snd b) + +type family Super c :: Constraint where + Super Type = () + Super (c, d) = (Category c, Category d) + +class Super cat => Category cat where + id :: forall (a :: cat). a ~> a + +instance Category Type where + id = \x -> x + +instance (Category c, Category d) => Category (c, d) where + id = ArrPair id id + +-- The commented out version worked +-- class Category (c, d) => Functor (f :: c -> d) where +class (Category c, Category d) => Functor (f :: c -> d) where + map :: (a ~> b) -> (f a ~> f b) + +data OnSnd f a b = OnSnd (f '(a, b)) + +instance Functor (f :: (c, d) -> Type) => Functor (OnSnd f a) where + map f (OnSnd x) = OnSnd (map (ArrPair id f) x) ===================================== testsuite/tests/typecheck/should_compile/all.T ===================================== @@ -939,3 +939,4 @@ test('T25960', normal, compile, ['']) test('T26020', normal, compile, ['']) test('T26020a', [extra_files(['T26020a_help.hs'])], multimod_compile, ['T26020a', '-v0']) test('T25992', normal, compile, ['']) +test('T14010', normal, compile, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/0515cc2fb2cd54d09786ab23cf99943... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/0515cc2fb2cd54d09786ab23cf99943... You're receiving this email because of your account on gitlab.haskell.org.