When compiling this program:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Kind
import Data.Type.Equality

foo :: forall (a :: Type) (b :: Type) (c :: Type).
       a :~~: b -> a :~~: c
foo HRefl = HRefl

GHC complains thus:

$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:12:13: error:
    • Could not deduce: a ~ c
      from the context: (* ~ *, b ~ a)
        bound by a pattern with constructor:
                   HRefl :: forall k1 (a :: k1). a :~~: a,
                 in an equation for ‘foo’
        at Bug.hs:12:5-9
      ‘a’ is a rigid type variable bound by
        the type signature for:
          foo :: forall a b c. (a :~~: b) -> a :~~: c
        at Bug.hs:(10,1)-(11,27)
      ‘c’ is a rigid type variable bound by
        the type signature for:
          foo :: forall a b c. (a :~~: b) -> a :~~: c
        at Bug.hs:(10,1)-(11,27)
      Expected type: a :~~: c
        Actual type: a :~~: a
    • In the expression: HRefl
      In an equation for ‘foo’: foo HRefl = HRefl
    • Relevant bindings include
        foo :: (a :~~: b) -> a :~~: c (bound at Bug.hs:12:1)
   |
12 | foo HRefl = HRefl
   |             ^^^^^

That * ~ * constraint is entirely redundant.