Opened 3 months ago

Closed 3 months ago

## #13879 closed bug (fixed)

# Strange interaction between higher-rank kinds and type synonyms

Reported by: | RyanGlScott | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | 8.2.1 |

Component: | Compiler (Type checker) | Version: | 8.0.1 |

Keywords: | TypeInType | Cc: | |

Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |

Type of failure: | GHC rejects valid program | Test Case: | typecheck/should_compile/T13879 |

Blocked By: | Blocking: | ||

Related Tickets: | Differential Rev(s): | ||

Wiki Page: |

### Description

Here's some code with typechecks with GHC 8.0.1, 8.0.2, 8.2.1, and HEAD:

{-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Kind data family Sing (a :: k) data (a :: j) :~~: (b :: k) where HRefl :: a :~~: a data instance Sing (z :: a :~~: b) where SHRefl :: Sing HRefl (%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type). Sing r -> p HRefl -> p r (%:~~:->) SHRefl pHRefl = pHRefl type App f x = f x type HRApp (f :: forall (z :: Type) (y :: z). a :~~: y -> Type) (x :: a :~~: b) = f x

Now I want to refactor this so that I use `App`

:

(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type). Sing r -> App p HRefl -> App p r

However, GHC doesn't like that:

$ /opt/ghc/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds -fprint-explicit-foralls GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:21:20: error: • Expected kind ‘(:~~:) j z a a’, but ‘'HRefl j a’ has kind ‘(:~~:) j j a a’ • In the second argument of ‘App’, namely ‘HRefl’ In the type signature: (%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type). Sing r -> App p HRefl -> App p r | 21 | -> App p HRefl | ^^^^^ Bug.hs:22:20: error: • Expected kind ‘(:~~:) j z a b’, but ‘r’ has kind ‘(:~~:) j k a b’ • In the second argument of ‘App’, namely ‘r’ In the type signature: (%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type). Sing r -> App p HRefl -> App p r | 22 | -> App p r | ^

These errors are surprising to me, since it appears that the two higher-rank types, `z`

and `y`

, are behaving differently here: `y`

appears to be willing to unify with other types in applications of `p`

, but `z`

isn't! I would expect *both* to be willing to unify in applications of `p`

.

Out of desperation, I tried this other formulation of `(%:~~:->)`

which uses `HRApp`

instead of `App`

:

(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type). Sing r -> HRApp p HRefl -> HRApp p r

But now I get an even stranger error message:

$ /opt/ghc/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds -fprint-explicit-foralls GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:21:20: error: • Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’, but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’ • In the first argument of ‘HRApp’, namely ‘p’ In the type signature: (%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type). Sing r -> HRApp p HRefl -> HRApp p r | 21 | -> HRApp p HRefl | ^ Bug.hs:21:20: error: • Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’, but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’ • In the first argument of ‘HRApp’, namely ‘p’ In the type signature: (%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type). Sing r -> HRApp p HRefl -> HRApp p r | 21 | -> HRApp p HRefl | ^ Bug.hs:22:20: error: • Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’, but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’ • In the first argument of ‘HRApp’, namely ‘p’ In the type signature: (%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type). Sing r -> HRApp p HRefl -> HRApp p r | 22 | -> HRApp p r | ^

That's right, it can't match the kinds:

`forall z (y :: z). (:~~:) j z a y -> *`

, and`forall z (y :: z). (:~~:) j z a y -> *`

Uh... what? Those are the same kind!

### Change History (7)

### comment:1 Changed 3 months ago by

### comment:5 Changed 3 months ago by

Status: | new → merge |
---|---|

Test Case: | → typecheck/should_compile/T13879 |

All done!

Probably worth merging these patches; I'm pretty sure they won't trigger new bugs.

### comment:6 Changed 3 months ago by

Milestone: | → 8.2.1 |
---|

### comment:7 Changed 3 months ago by

Resolution: | → fixed |
---|---|

Status: | merge → closed |

**Note:**See TracTickets for help on using tickets.

I could not resist investigating. Here are my conclusions.

`TcHsType.instantiateTyN`

. Easy to fix.`tcLHsKind`

(which converts the`LHsKind`

to a`Kind`

didn't zonk its result. Also easily fixed, and that makes the original program work.`HRApp`

. This arises because we try to unify the kinds (I'm using`HR`

instead of infix`:~~:`

, just to keep my head straight.) The first thing is that, at least by the time the constraint solver gets it, if we zonked LHS and RHS we'd see they were equal. But that's a small thing. What we do in`TcCanonical`

is this: Look at that`zipWithM`

. It's obvously bogus in the case above, because we produce a constraint`z1~z2`

which is insoluble.