Failure to resolve type parameter determined by type family

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

import Data.Proxy

-- Defined to get the type forall x . 'D x
data D where
  D :: a -> D

type family F t :: D

-- Will try to create values of this type through the type family
-- F, i.e. G (F t)
data G (d :: D) where
  G :: G ('D x)

-- This is rejected because the type variable x in 'D x is ambiguous.
-- But is it really? If there's an instance of F t then x is determined.
introG :: Proxy t -> G (F t)
introG _ = G

-- introG is well-typed if we add an equality constraint.
-- Can GHC not figure this out without our help?
introG' :: forall t x . ( F t ~ 'D x ) => Proxy t -> G (F t)
introG' _ = G

Here's the type error:

    • Couldn't match type ‘F t’ with ‘'D x0’
      Expected type: G (F t)
        Actual type: G ('D x0)
      The type variable ‘x0’ is ambiguous
    • In the expression: G
      In an equation for ‘introG’: introG _ = G

Trac metadata

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