GitLab

Load this file into GHCi:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
module Bug where

import Data.Type.Equality

pattern Foo = HRefl

$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )
Ok, 1 module loaded.
λ> :i Foo
pattern Foo :: () => (* ~ *, b ~ a) => a :~~: b

Notice that the type signature for Foo has an entirely redundant * ~ * constraint. The same does not happen if TypeInType is enabled.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeInType #-}
module Works where

import Data.Type.Equality

pattern Foo = HRefl

λ> :i Foo
pattern Foo :: forall k2 k1 (a :: k1) (b :: k2). () => (k2 ~ k1,
                                                        (b :: k2) ~~ (a :: k1)) => a :~~: b

Trac metadata

Trac field	Value
Version	8.2.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture