Richard Eisenberg

The following should compile, but doesn't. ``` {-# LANGUAGE PolyKinds, MultiParamTypeClasses, GADTs, ScopedTypeVariables, TypeOperators #-} {-# OPTIONS_GHC -fno-warn-redundant-constraints #-} module Super where import Data.Proxy import GHC.Prim class (a ~ b)...

Terrible error message from ->/~> confusion

1

Given ``` {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE PolyKinds #-} module TypeMap where import Unsafe.Coerce import Data.Type.Equality import...

Not that I expected it to work... ``` {-# LANGUAGE DeriveDataTypeable, TypeFamilies, TemplateHaskell, DataKinds, PolyKinds, GADTs, RankNTypes, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, CPP, FunctionalDependencies, StandaloneDeriving, TypeOperators, ScopedTypeVariables, NoMonomorphismRestriction, MonadComprehensions, DeriveGeneric, FlexibleContexts, GeneralizedNewtypeDeriving,...

``` {-# LANGUAGE PolyKinds, DataKinds, GADTs, TypeOperators, RankNTypes, MultiParamTypeClasses, ConstraintKinds #-} module Typeable where data (a :: k1) :~: (b :: k2) where Refl :: forall k (a :: k)....

``` {-# LANGUAGE PolyKinds, DataKinds, GADTs, TypeOperators, RankNTypes, MultiParamTypeClasses, ConstraintKinds #-} module Typeable where data (a :: k1) :~: (b :: k2) where Refl :: forall k (a :: k)....

This fails with a panic: ``` import Data.Proxy data T a where Foo :: Show a => a -> T a type Blah = 'Foo True ```

This fails, but it looks right to me: ``` {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE ExistentialQuantification #-} {-#...

`:k (#,,#)` says `* -> * -> * -> #`. But that's wrong.

For example, when I say `:k (Any :: TYPE Lifted)`, I get a complaint. It works with `'Lifted`.

``` data A data B :: A -> * data C :: B a -> * data D :: C b -> * data E :: D c -> *...