diff options
author | Ryan Scott <ryan.gl.scott@gmail.com> | 2019-07-26 19:05:35 -0400 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2019-10-07 12:00:59 -0400 |
commit | 825c108bd26f20accf1eaef2ba652a2ee12924bb (patch) | |
tree | 3af901344da47b45fc041664c3af59188e113bb4 /testsuite/tests/typecheck | |
parent | 241921a0c238a047326b0c0f599f1c24222ff66c (diff) | |
download | haskell-825c108bd26f20accf1eaef2ba652a2ee12924bb.tar.gz |
Only flatten up to type family arity in coreFlattenTyFamApp (#16995)
Among other uses, `coreFlattenTyFamApp` is used by Core Lint as a
part of its check to ensure that each type family axiom reduces
according to the way it is defined in the source code. Unfortunately,
the logic that `coreFlattenTyFamApp` uses to flatten type family
applications disagreed with the logic in `TcFlatten`, which caused
it to spuriously complain this program:
```hs
type family Param :: Type -> Type
type family LookupParam (a :: Type) :: Type where
LookupParam (f Char) = Bool
LookupParam x = Int
foo :: LookupParam (Param ())
foo = 42
```
This is because `coreFlattenTyFamApp` tries to flatten the `Param ()`
in `LookupParam (Param ())` to `alpha` (where `alpha` is a flattening
skolem), and GHC is unable to conclude that `alpha` is apart from
`f Char`. This patch spruces up `coreFlattenTyFamApp` so that it
instead flattens `Param ()` to `alpha ()`, which GHC _can_ know for
sure is apart from `f Char`. See
`Note [Flatten], wrinkle 3` in `FamInstEnv`.
Diffstat (limited to 'testsuite/tests/typecheck')
-rw-r--r-- | testsuite/tests/typecheck/should_compile/T16995.hs | 21 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 1 |
2 files changed, 22 insertions, 0 deletions
diff --git a/testsuite/tests/typecheck/should_compile/T16995.hs b/testsuite/tests/typecheck/should_compile/T16995.hs new file mode 100644 index 0000000000..737ddbe066 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T16995.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE TypeFamilies #-} +module T16995 where + +import Data.Kind + +type family Param1 :: Type -> Type +type family Param2 (a :: Type) :: Type -> Type +type family Param3 (a :: Type) (b :: Type) :: Type -> Type + +type family LookupParam (a :: Type) :: Type where + LookupParam (_ Char) = Bool + LookupParam _ = Int + +foo :: LookupParam (Param1 Bool) +foo = 42 + +bar :: LookupParam (Param2 Bool Bool) +bar = 27 + +baz :: LookupParam (Param3 Bool Bool Bool) +baz = 12 diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 30a64518fe..ee38a1abea 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -686,6 +686,7 @@ test('UnliftedNewtypesLPFamily', normal, compile, ['']) test('UnliftedNewtypesDifficultUnification', normal, compile, ['']) test('T16832', normal, ghci_script, ['T16832.script']) test('T16946', normal, compile, ['']) +test('T16995', normal, compile, ['']) test('T17007', normal, compile, ['']) test('T17067', normal, compile, ['']) test('T17202', expect_broken(17202), compile, ['']) |