Opened 13 months ago

Closed 9 months ago

## #14556 closed bug (fixed)

# Core Lint error: Ill-kinded result in coercion

Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | |

Component: | Compiler | Version: | 8.3 |

Keywords: | TypeInType | Cc: | |

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

Type of failure: | None/Unknown | Test Case: | dependent/should_compile/T14556 |

Blocked By: | Blocking: | ||

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

Wiki Page: |

### Description

{-# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-} import Data.Kind import Data.Proxy data Fn a b where IdSym :: Fn Type Type type family (@@) (f::Fn k k') (a::k)::k' where IdSym @@ a = a data KIND = X | FNARR KIND KIND data TY :: KIND -> Type where ID :: TY (FNARR X X) FNAPP :: TY (FNARR k k') -> TY k -> TY k' data TyRep (kind::KIND) :: TY kind -> Type where TID :: TyRep (FNARR X X) ID TFnApp :: TyRep (FNARR k k') f -> TyRep k a -> TyRep k' (FNAPP f a) type family IK (kind::KIND) :: Type where IK X = Type IK (FNARR k k') = Fn (IK k) (IK k') type family IT (ty::TY kind) :: IK kind where IT ID = IdSym IT (FNAPP f x) = IT f @@ IT x zero :: TyRep X a -> IT a zero = undefined

which gives Core lint error when run with `ghci -ignore-dot-ghci -dcore-lint`

(8.3.20171122) attached.

It compiles fine with

zero :: TyRep X a -> IT a zero = zero

but fails with `zero = let x = x in x`

. See #14554.

### Attachments (1)

### Change History (4)

### Changed 13 months ago by

### comment:1 Changed 12 months ago by

### comment:3 Changed 9 months ago by

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

Status: | new → closed |

Test Case: | → dependent/should_compile/T14556 |

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

I think this is another example of the bugs surrounding "flattened types have flattened kinds". What is happening is this. In the RHS of

`zero`

we get a constraintwhich should strainghtforwardly unify. But before we do that we flatten

`(IT a |> ax_IK)`

, but alas we get justThe cast has disappeared. This happens in

`TcFlatten`

:I'm pretty sure it's just another manifestation of our existing set of bugs around flattening (Trac #12919). Richard has a mostly-finished patch that cures this --- it'd be great to get it finished!